# HG changeset patch
# User wenzelm
# Date 1518257968 -3600
# Node ID 5fcd6aad8e6b638655d12c0f2bdb7e8a93fb8b66
# Parent  8b19a8a7f029426f5967548a8d63991958774a01
tuned;

diff -r 8b19a8a7f029 -r 5fcd6aad8e6b src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Fri Feb 09 17:57:36 2018 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Sat Feb 10 11:19:28 2018 +0100
@@ -187,20 +187,20 @@
 
     {
       val polyc_path = target + Path.explode("polyc")
+
+      val Header = "#! */bin/sh".r
       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\""
+          case Header() :: lines =>
+            val lines1 =
+              lines.map(line =>
+                if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\""
+                else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\""
                 else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\""
                 else line)
-            cat_lines(a1 :: b1 :: rest1)
+            cat_lines("#!/usr/bin/env bash" ::lines1)
           case lines =>
-            error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(6)))
+            error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3)))
         }
       File.write(polyc_path, polyc_patched)
     }