diff options
Diffstat (limited to 'doc/changelog/08-tools/11851-coqc-flags-fix.rst')
| -rw-r--r-- | doc/changelog/08-tools/11851-coqc-flags-fix.rst | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst deleted file mode 100644 index ff736641b4..0000000000 --- a/doc/changelog/08-tools/11851-coqc-flags-fix.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - 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). |