diff options
| author | Théo Zimmermann | 2020-05-12 14:54:41 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-13 12:26:57 +0200 |
| commit | 684bbe55e9ee94f93486da6d2df97fcef3136d88 (patch) | |
| tree | fdabedc6cbeb43a2109234d11d2e777f8d726b2c /doc/changelog | |
| parent | bd78f3282f76c31a7579dc667732821a9aac889c (diff) | |
Document the changes regarding the order of command-line options.
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/08-tools/11851-coqc-flags-fix.rst | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst index a07e48d2d8..ff736641b4 100644 --- a/doc/changelog/08-tools/11851-coqc-flags-fix.rst +++ b/doc/changelog/08-tools/11851-coqc-flags-fix.rst @@ -1,6 +1,9 @@ - **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>`_, + The order in which the require flags `-ri`, `-re`, `-rfrom`, etc. + and the option flags `-set`, `-unset` are given now matters. In + particular, it is now possible to interleave the loading of plugins + and the setting of options by choosing the right order for these + flags. The load flags `-l` and `-lv` are still processed afterward + for now (`#11851 <https://github.com/coq/coq/pull/11851>`_ and + `#12097 <https://github.com/coq/coq/pull/12097>`_, by Lasse Blaauwbroek). |