diff options
| author | Hugo Herbelin | 2019-05-08 13:22:34 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 02:31:26 +0200 |
| commit | fe5389542af2d9b6e8d964bbc2c10e997af409fe (patch) | |
| tree | d04d6e75273a7bc55291f5b791ed260a6024eed3 /toplevel/coqloop.ml | |
| parent | 5f3777e9ca29493a242b66f92ba803fa5760a634 (diff) | |
A classification of command line options.
A few semantic changes:
- several queries (-where, -config, ...) are accepted
- queries are exclusive of other arguments
- option -filterops is exclusive of other arguments if it contains
another query (this allows to get rid of the "exitcode" hack)
Diffstat (limited to 'toplevel/coqloop.ml')
| -rw-r--r-- | toplevel/coqloop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 4bcde566e3..f6211102e6 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -444,7 +444,7 @@ let drop_args = ref None let loop ~opts ~state = drop_args := Some opts; let open Coqargs in - print_emacs := opts.print_emacs; + print_emacs := opts.config.print_emacs; (* We initialize the console only if we run the toploop_run *) let tl_feed = Feedback.add_feeder coqloop_feed in if Dumpglob.dump () then begin |