diff options
| author | Emilio Jesus Gallego Arias | 2020-03-22 00:31:28 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-22 00:31:28 -0400 |
| commit | b048ecb6d874e1eb2e33c1fa3a15d3a508500285 (patch) | |
| tree | 5ab0bb6e675b72b39302ec581962f40e1eaec77d /doc/changelog | |
| parent | ec4b889aa4e837bd82a7d0a059d0c967cde1ac46 (diff) | |
| parent | 3e98d9bd37d629f90e0a5702f6deb5b835815b5a (diff) | |
Merge PR #11851: Process command line load vernaculars before command line Goptions
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/08-tools/11851-coqc-flags-fix.rst | 6 |
1 files changed, 6 insertions, 0 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). |