From e5c4bc888c1f0516928a32f70529f95e36243c5d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 1 Nov 2010 07:46:32 +0000
Subject: Restored checking that _all_ arguments of the command line are
 meaningful

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13600 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/coqtop.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 864bf2e35b..6d98d3dd0c 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -293,7 +293,11 @@ let parse_args arglist =
 
     | "-filteropts" :: rem -> filter_opts := true; parse rem
 
-    | s :: rem -> s :: (parse rem)
+    | s :: rem ->
+      if !filter_opts then
+       s :: (parse rem)
+      else
+       (prerr_endline ("Don't know what to do with " ^ s); usage ())
   in
   try
     parse arglist
@@ -314,7 +318,6 @@ let init arglist =
       let foreign_args = parse_args arglist in
       if !filter_opts then
         (print_string (String.concat "\n" foreign_args); exit 0);
-      (* no else. ignore additional options. makes life easier *)
       if !ide_slave then begin
         Flags.make_silent true;
         Pfedit.set_undo (Some 5000);
-- 
cgit v1.2.3