--- a/src/Pure/Admin/component_polyml.scala Wed Apr 09 16:55:20 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala Wed Apr 09 17:40:27 2025 +0200
@@ -31,7 +31,7 @@
Platform_Info(
options =
List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
- setup = MinGW.environment_export,
+ setup = MinGW.env_prefix(),
libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread")))
sealed case class Platform_Context(
--- a/src/Pure/System/bash.scala Wed Apr 09 16:55:20 2025 +0200
+++ b/src/Pure/System/bash.scala Wed Apr 09 17:40:27 2025 +0200
@@ -42,6 +42,9 @@
def strings(ss: Iterable[String]): String =
ss.iterator.map(Bash.string).mkString(" ")
+ def exports(environment: String*): String =
+ environment.iterator.map(a => "export " + string(a)).mkString("", "\n", "\n")
+
/* process and result */
--- a/src/Pure/System/mingw.scala Wed Apr 09 16:55:20 2025 +0200
+++ b/src/Pure/System/mingw.scala Wed Apr 09 17:40:27 2025 +0200
@@ -8,11 +8,12 @@
object MinGW {
- def environment: List[String] =
- List("PATH=/usr/bin:/bin:/mingw64/bin", "CONFIG_SITE=/mingw64/etc/config.site")
-
- def environment_export: String =
- environment.map(a => "export " + Bash.string(a)).mkString("", "\n", "\n")
+ def env_prefix(pre_path: String = "", post_path: String = ""): String = {
+ val path =
+ if_proper(pre_path, pre_path + ":") + "/usr/bin:/bin:/mingw64/bin" +
+ if_proper(post_path, ":" + post_path)
+ Bash.exports("PATH=" + path, "CONFIG_SITE=/mingw64/etc/config.site")
+ }
val none: MinGW = new MinGW(None)
def apply(path: Path) = new MinGW(Some(path))
@@ -37,12 +38,12 @@
case _ => File.standard_path(path)
}
- def bash_script(script: String): String =
+ def bash_script(script: String, env_prefix: String = MinGW.env_prefix()): String =
root match {
case None => script
case Some(msys_root) =>
File.bash_path(msys_root + Path.explode("usr/bin/bash")) +
- " -c " + Bash.string(MinGW.environment_export + script)
+ " -c " + Bash.string(env_prefix + script)
}
def get_root: Path =