aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--lib/cWarnings.ml8
-rw-r--r--toplevel/coqtop.ml7
2 files changed, 12 insertions, 3 deletions
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index ff71452672..3699b1c614 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -93,8 +93,12 @@ let split_flags s =
"all" flag, and reverses the list. *)
let rec cut_before_all_rev acc = function
| [] -> acc
- | (_status,name as w) :: warnings ->
- cut_before_all_rev (w :: if is_all_keyword name then [] else acc) warnings
+ | (status,name as w) :: warnings ->
+ let acc =
+ if is_all_keyword name then [w]
+ else if is_none_keyword name then [(Disabled,"all")]
+ else w :: acc in
+ cut_before_all_rev acc warnings
let cut_before_all_rev warnings = cut_before_all_rev [] warnings
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c1cdaa5a34..db7bcb76b1 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 *)