From 492ad5ad0b4c55610c9896436d2165ac22b527a6 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 23 Aug 2012 12:52:47 +0000
Subject: No more coqtop.opt, produce directly a coqtop binary

 We now always produce two binaries, coqtop and coqtop.byte :
 - If ocamlopt is available, coqtop is directly what used to be coqtop.opt,
   no more symlinks needed.
 - Otherwise, coqtop is a copy of coqtop.byte.

 The same for coqchk and coqide...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15752 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 scripts/coqc.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'scripts')

diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 5a0c0623ca..0a3938ae13 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -22,8 +22,7 @@
 
 let environment = Unix.environment ()
 
-let best = if Coq_config.arch = "win32" then "" else ("."^Coq_config.best)
-let binary = ref ("coqtop" ^ best)
+let binary = ref "coqtop"
 let image = ref ""
 
 (* coqc options *)
@@ -110,8 +109,7 @@ let parse_args () =
 	usage ()
     | "-byte" :: rem ->
        binary := "coqtop.byte"; parse (cfiles,args) rem
-    | "-opt" :: rem ->
-       binary := "coqtop.opt"; parse (cfiles,args) rem
+    | "-opt" :: rem -> (* now a no-op *) parse (cfiles,args) rem
     | "-libdir" :: _ :: rem ->
         print_string "Warning: option -libdir deprecated and ignored\n"; flush stdout;
         parse (cfiles,args) rem
-- 
cgit v1.2.3