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.
---
 lib/system.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'lib/system.ml')

diff --git a/lib/system.ml b/lib/system.ml
index eef65a4e3d..902a4f2506 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -301,8 +301,11 @@ let with_time ~batch f x =
     Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
 
+(* We use argv.[0] as we don't want to resolve symlinks *)
 let get_toplevel_path top =
-  let dir = Filename.dirname Sys.executable_name in
+  let open Filename in
+  let dir = if String.equal (basename Sys.argv.(0)) Sys.argv.(0)
+            then "" else dirname Sys.argv.(0) ^ dir_sep in
   let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in
   let eff = if Dynlink.is_native then ".opt" else ".byte" in
-  dir ^ Filename.dir_sep ^ top ^ eff ^ exe
+  dir ^ top ^ eff ^ exe
-- 
cgit v1.2.3