# HG changeset patch
# User wenzelm
# Date 1518192691 -3600
# Node ID 252d33ee6778a141200319f7fce8d33292261b3c
# Parent  c933a5d4e1eebbe8a06bffcfb2309596f6c843f6
patch polyc: avoid hardwired directory prefix;

diff -r c933a5d4e1ee -r 252d33ee6778 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Fri Feb 09 16:27:52 2018 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Fri Feb 09 17:11:31 2018 +0100
@@ -169,7 +169,7 @@
       File.copy(Path.explode(file).expand_env(settings), target)
 
 
-    /* built-in library path */
+    /* poly: library path */
 
     if (Platform.is_linux) {
       bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check
@@ -181,6 +181,29 @@
             Bash.string("@executable_path/" + Path.explode(file).base_name) + " poly").check
       }
     }
+
+
+    /* polyc: directory prefix */
+
+    {
+      val polyc_path = target + Path.explode("polyc")
+      val polyc_patched =
+        split_lines(File.read(polyc_path)) match {
+          case a :: b :: rest
+          if "#! */bin/sh".r.pattern.matcher(a).matches && b.startsWith("prefix=") =>
+            val a1 = "#!/usr/bin/env bash"
+            val b1 = "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\""
+            val rest1 =
+              rest.map(line =>
+                if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\""
+                else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\""
+                else line)
+            cat_lines(a1 :: b1 :: rest1)
+          case lines =>
+            error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(6)))
+        }
+      File.write(polyc_path, polyc_patched)
+    }
   }