aboutsummaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
authorvgross2010-09-14 14:43:01 +0000
committervgross2010-09-14 14:43:01 +0000
commitc9a9752c76bfb592d775a7fdb9ebe4702ff1aaef (patch)
tree10bf7c57d0ae1c66481d1ea72a4dd438ebc5525e /scripts
parent4b6b6ba87ee19854bb8464cb248fcf40f0b965e1 (diff)
CoqIDE argv parsing delegated to coqtop
Introduces some hacks to have a consistent user experience. When coqtop prints info on self then exit, return code is 2 if called with -filteropts, 0 else For now, no options are accepted by coqide. there is no way for now to specify a filename that begins with a dash. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13415 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqc.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 1d5ba7f118..eb33850a7b 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -163,7 +163,7 @@ let parse_args () =
| ("-config" | "--config") :: _ -> Usage.print_config (); exit 0
| ("-v"|"--version") :: _ ->
- Usage.version ()
+ Usage.version 0
| f :: rem ->
if Sys.file_exists f then
parse (f::cfiles,args) rem