From 88c4a5a2958e2c0bbd2d142e684dc642946e2e41 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 21 Sep 2017 13:41:56 +0200
Subject: Handle multiple -w options on command line (bug #5736).

---
 toplevel/coqtop.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0f8524e923..712efbbd5b 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 *)
-- 
cgit v1.2.3


From 9c016084a178ebb02f51ffdd2f7cc7c7a98afa4b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 21 Sep 2017 14:10:51 +0200
Subject: Improve support for "-w none" compatibility option.

If coqtop was started with "-w none" yet the script used "Set Warnings
Append", then all the warnings were turned back to their default value.
This commit turns "none" (whatever its sign) into "-all" whenever some
warning status is modified afterward, in order to prevent the issue.
---
 lib/cWarnings.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 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
 
-- 
cgit v1.2.3