diff options
| author | Björn Persson <bjorn@rombobjörn.se> | 2013-10-21 20:37:27 +0200 |
|---|---|---|
| committer | Björn Persson <bjorn@rombobjörn.se> | 2013-10-21 20:37:27 +0200 |
| commit | 673d971de175a4895b7f010b738294d3a40dc0d7 (patch) | |
| tree | f1f2f605381ca6e1fdb98e00e663654924eac1ea | |
| parent | c2e343aede23579a76c02469e5594410928ee563 (diff) | |
minor clarification
| -rwxr-xr-x | manual.en.html | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/manual.en.html b/manual.en.html index 59bd42b..92988e8 100755 --- a/manual.en.html +++ b/manual.en.html @@ -453,7 +453,8 @@ file is preprocessed, and <var>builder_arguments</var> will be passed to GPRbuild or Gnatmake when a project is built. These variables are not meant to be overridden by users. They may be used for preprocessor symbols, external variables for project files or other arguments that are essential for the build -to work. Global default values for optional arguments should be set in the +to work. (Essential arguments may of course also be specified in build project +files.) Global default values for optional arguments should be set in the options variables instead.</p> <p>The program-name variables <var>GNATPREP</var> and <var>GNAT_BUILDER</var> |