From 3e98d9bd37d629f90e0a5702f6deb5b835815b5a Mon Sep 17 00:00:00 2001 From: Lasse Blaauwbroek Date: Tue, 17 Mar 2020 22:59:23 +0100 Subject: 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. --- doc/changelog/08-tools/11851-coqc-flags-fix.rst | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 doc/changelog/08-tools/11851-coqc-flags-fix.rst (limited to 'doc/changelog') 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 `_, + by Lasse Blaauwbroek). -- cgit v1.2.3