diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-01 07:46:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-01 07:46:32 +0000 |
| commit | e5c4bc888c1f0516928a32f70529f95e36243c5d (patch) | |
| tree | 43ee8671df26fcce864a27624fc7ee9ee87a2fb9 | |
| parent | d5b8d399b8de3e13180035401dde85a3effa8d53 (diff) | |
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
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 864bf2e35..6d98d3dd0 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); |