aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-05 19:41:32 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-05 19:41:32 +0200
commit2aac4ae818fec0d409da31ef9da83796d871d687 (patch)
treef01c726982850aace7761a79324abeee775482ea /toplevel
parent9c033b4da738fb399eebe9f8ccf0f8a407d6d42e (diff)
parent9c016084a178ebb02f51ffdd2f7cc7c7a98afa4b (diff)
Merge PR #1069: Improve support for -w options
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml7
1 files changed, 6 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c1cdaa5a3..db7bcb76b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -539,7 +539,12 @@ let parse_args arglist =
|"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
|"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Flags.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 *)