aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5ae1c36ed..d9f8ed881 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -524,7 +524,7 @@ 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 (next ())
+ |"-w" | "-W" -> CWarnings.set_flags (CWarnings.normalize_flags_string (next ()))
|"-o" -> Flags.compilation_output_name := Some (next())
(* Options with zero arg *)