From 340088bbc08d5a3f55110dc2d287a83866ad2740 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 5 Sep 2018 20:12:23 +0200
Subject: [bin] Fix binary location procedure to work with symlinks.

In #7860 `Sys.executable_name` was introduced to locate coq private
binaries; however, this breaks use cases with symlinks, such as Dune.

In order to fix this, we adopt a simpler strategy; we will always
adapt the name originally provided by the user, and only add a
directory if it was originally present.

This should work (hopefully) in all cases.

This fixes `coqide` not working on Dune builds.
---
 ide/ideutils.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'ide')

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 960beb8455..e84779d26d 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -328,15 +328,18 @@ let coqtop_path () =
       | None ->
         try
           let new_prog = System.get_toplevel_path "coqidetop" in
-            if Sys.file_exists new_prog then new_prog
+            (* The file exists or it is to be found by path *)
+            if Sys.file_exists new_prog ||
+               CString.equal Filename.(basename new_prog) new_prog
+            then new_prog
 	    else
 	      let in_macos_bundle =
 		Filename.concat
 		  (Filename.dirname new_prog)
 		  (Filename.concat "../Resources/bin" (Filename.basename new_prog))
 	      in if Sys.file_exists in_macos_bundle then in_macos_bundle
-                 else "coqidetop"
-        with Not_found -> "coqidetop"
+                 else "coqidetop.opt"
+        with Not_found -> "coqidetop.opt"
   in file
 
 (* In win32, when a command-line is to be executed via cmd.exe
-- 
cgit v1.2.3