diff options
| author | Lasse Blaauwbroek | 2020-03-17 22:59:23 +0100 |
|---|---|---|
| committer | Lasse Blaauwbroek | 2020-03-21 14:31:20 +0100 |
| commit | 3e98d9bd37d629f90e0a5702f6deb5b835815b5a (patch) | |
| tree | 8f5547edeba39bd3a47a9dfea72038da41c90ec3 /doc | |
| parent | 4d025d4161599ea20cd1dbf489a6412f019a7a7e (diff) | |
Reorder the load/require cmd-options and set/unset cmd-options
Make sure that all initial load vernaculars that were specified on the command line are executed before processing the options set through -set on the command line.
The reason for this is that the load vernacular options can load plugins that define new Goptions. If these plugins are not loaded before the -set flags are processed,
then Goptions will emit a warning that the options of that plugin don't exist and ignore the flag.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/08-tools/11851-coqc-flags-fix.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 5 |
2 files changed, 10 insertions, 1 deletions
diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst new file mode 100644 index 0000000000..a07e48d2d8 --- /dev/null +++ b/doc/changelog/08-tools/11851-coqc-flags-fix.rst @@ -0,0 +1,6 @@ +- **Changed:** + The order in which the require/load flags `-l`, `-ri`, `-re`, `-rfrom`, etc. + and the option set flags `-set`, `-unset` are processed have been reversed. + In the new behavior, require/load flags are processed before option flags. + (`#11851 <https://github.com/coq/coq/pull/11851>`_, + by Lasse Blaauwbroek). diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 98d222e317..aa4b6edd7d 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -227,7 +227,10 @@ and ``coqtop``, unless stated otherwise: type of the option. For flags ``Option Name`` is equivalent to ``Option Name=true``. For instance ``-set "Universe Polymorphism"`` will enable :flag:`Universe Polymorphism`. Note that the quotes are - shell syntax, Coq does not see them. + shell syntax, Coq does not see them. Flags are processed after initialization + of the document. This includes the `Prelude` if loaded and any libraries loaded + through the `-l`, `-lv`, `-r`, `-re`, `-ri`, `rfrom`, `-refrom` and `-rifrom` + options. :-unset *string*: As ``-set`` but used to disable options and flags. :-compat *version*: Attempt to maintain some backward-compatibility with a previous version. |