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/sphinx/practical-tools/coq-commands.rst | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx')

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.
-- 
cgit v1.2.3