diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-09-21 13:41:56 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-09-21 13:55:06 +0200 |
| commit | 88c4a5a2958e2c0bbd2d142e684dc642946e2e41 (patch) | |
| tree | c578d50a295d06788e4ef7ca0b41c7c07e7eac93 /toplevel | |
| parent | 9933871efd122163f7e2dfe8377b9b2dd384b47b (diff) | |
Handle multiple -w options on command line (bug #5736).
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0f8524e92..712efbbd5 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -540,7 +540,12 @@ let parse_args arglist = |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo |"-toploop" -> set_toploop (next ()) - |"-w" | "-W" -> CWarnings.set_flags (CWarnings.normalize_flags_string (next ())) + |"-w" | "-W" -> + let w = next () in + if w = "none" then CWarnings.set_flags w + else + let w = CWarnings.get_flags () ^ "," ^ w in + CWarnings.set_flags (CWarnings.normalize_flags_string w) |"-o" -> Flags.compilation_output_name := Some (next()) (* Options with zero arg *) |