aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-09-27 15:46:21 +0200
committerEmilio Jesus Gallego Arias2018-09-27 15:57:54 +0200
commit686503bfe85436e5af927a02f7e1fb0bf2f975c9 (patch)
tree2638e6b734f50414e38b87598ea85d177e552719 /tools
parent64a8f3cbb2fa278ed9d7bf2e5567d4e2b9bfa9dc (diff)
[coqc] Use standard binary location routine from lib
Instead of rolling our own, we use the standard one that works well when binaries are symlinked.
Diffstat (limited to 'tools')
-rw-r--r--tools/coqc.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 90d8e67c1e..2cbf05bd8b 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -24,7 +24,7 @@
let environment = Unix.environment ()
-let binary = ref "coqtop"
+let use_bytecode = ref false
let image = ref ""
let verbose = ref false
@@ -69,8 +69,8 @@ let parse_args () =
verbose := true ; parse (cfiles,args) rem
| "-image" :: f :: rem -> image := f; parse (cfiles,args) rem
| "-image" :: [] -> usage ()
- | "-byte" :: rem -> binary := "coqtop.byte"; parse (cfiles,args) rem
- | "-opt" :: rem -> binary := "coqtop"; parse (cfiles,args) rem
+ | "-byte" :: rem -> use_bytecode := true; parse (cfiles,args) rem
+ | "-opt" :: rem -> use_bytecode := false; parse (cfiles,args) rem
(* Informative options *)
@@ -155,7 +155,7 @@ let main () =
end;
let coqtopname =
if !image <> "" then !image
- else Filename.concat Envars.coqbin (!binary ^ Coq_config.exec_extension)
+ else System.get_toplevel_path ~byte:!use_bytecode "coqtop"
in
(* List.iter (compile coqtopname args) cfiles*)
Unix.handle_unix_error (compile coqtopname args) cfiles