# HG changeset patch
# User wenzelm
# Date 1602358434 -7200
# Node ID def95a34df8e96641d6c454370d6c03b3fb7911d
# Parent  f5d60c12deeb2850ed500d481733462f373dfe1c
clarified signature;

diff -r f5d60c12deeb -r def95a34df8e src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Sat Oct 10 21:19:22 2020 +0200
+++ b/src/Pure/Admin/build_polyml.scala	Sat Oct 10 21:33:54 2020 +0200
@@ -37,9 +37,7 @@
       Platform_Info(
         options =
           List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
-        setup =
-          """PATH=/usr/bin:/bin:/mingw64/bin
-            export CONFIG_SITE=/mingw64/etc/config.site""",
+        setup = MinGW.environment_export,
         copy_files =
           List("$MSYS/mingw64/bin/libgcc_s_seh-1.dll",
             "$MSYS/mingw64/bin/libgmp-10.dll",
diff -r f5d60c12deeb -r def95a34df8e src/Pure/System/mingw.scala
--- a/src/Pure/System/mingw.scala	Sat Oct 10 21:19:22 2020 +0200
+++ b/src/Pure/System/mingw.scala	Sat Oct 10 21:33:54 2020 +0200
@@ -9,12 +9,14 @@
 
 object MinGW
 {
-  def environment: List[(String, String)] =
-    List("PATH" -> "/usr/bin:/bin:/mingw64/bin", "CONFIG_SITE" -> "/mingw64/etc/config.site")
+  def environment: List[String] =
+    List("PATH=/usr/bin:/bin:/mingw64/bin", "CONFIG_SITE=/mingw64/etc/config.site")
 
   def environment_prefix: String =
-    (for ((a, b) <- environment) yield Bash.string(a) + "=" + Bash.string(b))
-      .mkString("/usr/bin/env ", " ", " ")
+    environment.map(Bash.string).mkString("/usr/bin/env ", " ", " ")
+
+  def environment_export: String =
+    environment.map(a => "export " + Bash.string(a)).mkString("", "\n", "\n")
 
   val none: MinGW = new MinGW(None)
   def root(path: Path) = new MinGW(Some(path))