From 686503bfe85436e5af927a02f7e1fb0bf2f975c9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 27 Sep 2018 15:46:21 +0200
Subject: [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.
---
 tools/coqc.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tools')

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
-- 
cgit v1.2.3