src/Pure/Admin/build_polyml.scala
changeset 75202 4fdde010086f
parent 74635 b179891dd357
child 75205 c33e75542ffe
equal deleted inserted replaced
75201:8f6b8a46f54c 75202:4fdde010086f
   126 
   126 
   127 
   127 
   128     /* polyc: directory prefix */
   128     /* polyc: directory prefix */
   129 
   129 
   130     val Header = "#! */bin/sh".r
   130     val Header = "#! */bin/sh".r
   131     File.change(platform_dir + Path.explode("polyc"), txt =>
   131     File.change(platform_dir + Path.explode("polyc")) { text =>
   132       split_lines(txt) match {
   132       split_lines(text) match {
   133         case Header() :: lines =>
   133         case Header() :: lines =>
   134           val lines1 =
   134           val lines1 =
   135             lines.map(line =>
   135             lines.map(line =>
   136               if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\""
   136               if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\""
   137               else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\""
   137               else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\""
   138               else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\""
   138               else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\""
   139               else line)
   139               else line)
   140           cat_lines("#!/usr/bin/env bash" ::lines1)
   140           cat_lines("#!/usr/bin/env bash" :: lines1)
   141         case lines =>
   141         case lines =>
   142           error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3)))
   142           error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3)))
   143       }
   143       }
   144     )
   144     }
   145   }
   145   }
   146 
   146 
   147 
   147 
   148 
   148 
   149   /** skeleton for component **/
   149   /** skeleton for component **/