src/Pure/System/mingw.scala
changeset 82465 3cc075052033
parent 82463 3125fd1ee69c
child 82467 b0740dce1f1d
--- 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 =