aboutsummaryrefslogtreecommitdiffhomepage
path: root/scripts
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-24 08:20:43 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-24 08:20:43 +0000
commitf0d9eaa042f47eb5d5c358ae41df185fe5b05bf9 (patch)
treeb9a54b4f1ab7728cd858a87c38df511396f8aa0b /scripts
parent2e68487cf52e6a853cdd61bce22e7836afdd3821 (diff)
- coqc: utilise le meilleur coq possible
- coqc -v réparé - coqtop: options -byte et -opt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@940 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqc.ml8
1 files changed, 6 insertions, 2 deletions
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 85cea9606..adc521232 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -18,7 +18,7 @@
let environment = Unix.environment ()
let bindir = ref Coq_config.bindir
-let binary = ref "coqtop.byte"
+let binary = ref ("coqtop." ^ Coq_config.best)
(* the $COQBIN environment variable has priority over the Coq_config value *)
let _ =
@@ -133,8 +133,12 @@ let parse_args () =
end
| ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois"
|"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
- |"-silent"|"-v"|"--version" as o) :: rem ->
+ |"-silent" as o) :: rem ->
parse (cfiles,o::args) rem
+ | ("-v"|"--version") :: _ ->
+ Usage.version ()
+ | "-where" :: _ ->
+ print_endline Coq_config.coqlib; exit 0
| f :: rem ->
if Sys.file_exists f then
parse (f::cfiles,args) rem