diff options
| author | Gaëtan Gilbert | 2019-02-08 13:34:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-08 13:34:02 +0100 |
| commit | 6c06f36b2dd1812454d40cbde1da28e1ea8be67e (patch) | |
| tree | 62782d00b4c5781caf89dfc08e804f220e6cc790 /toplevel/usage.ml | |
| parent | 99c1d7b0ae1beed66fe8dd6a06db84dc0c8322d8 (diff) | |
Make boot flag into a normal option (no global flag).
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 277f8b7367..0d17218a56 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -62,7 +62,7 @@ let print_usage_common co command = \n\ \n -q skip loading of rcfile\ \n -init-file f set the rcfile to f\ -\n -boot boot mode (allows to overload the `Coq` library prefix)\ +\n -boot boot mode (allows to overload the `Coq` library prefix, implies -q)\ \n -bt print backtraces (requires configure debug flag)\ \n -debug debug mode (implies -bt)\ \n -diffs (on|off|removed) highlight differences between proof steps\ |