# HG changeset patch
# User wenzelm
# Date 1602359158 -7200
# Node ID b7351ffe0dbc3a97109f37fd2c722aef80712317
# Parent  def95a34df8e96641d6c454370d6c03b3fb7911d
clarified signature: allow complex bash script;

diff -r def95a34df8e -r b7351ffe0dbc src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala	Sat Oct 10 21:33:54 2020 +0200
+++ b/src/Pure/Admin/build_csdp.scala	Sat Oct 10 21:45:58 2020 +0200
@@ -123,7 +123,7 @@
             foreach(file => flags.change(File.path(file)))
       }
 
-      progress.bash(mingw.bash_command("make"), cwd = build_dir.file, echo = verbose).check
+      progress.bash(mingw.bash_script("make"), cwd = build_dir.file, echo = verbose).check
 
 
       /* install */
diff -r def95a34df8e -r b7351ffe0dbc src/Pure/System/mingw.scala
--- a/src/Pure/System/mingw.scala	Sat Oct 10 21:33:54 2020 +0200
+++ b/src/Pure/System/mingw.scala	Sat Oct 10 21:45:58 2020 +0200
@@ -12,9 +12,6 @@
   def environment: List[String] =
     List("PATH=/usr/bin:/bin:/mingw64/bin", "CONFIG_SITE=/mingw64/etc/config.site")
 
-  def environment_prefix: String =
-    environment.map(Bash.string).mkString("/usr/bin/env ", " ", " ")
-
   def environment_export: String =
     environment.map(a => "export " + Bash.string(a)).mkString("", "\n", "\n")
 
@@ -30,12 +27,12 @@
       case Some(msys_root) => "MinGW.root(" + msys_root.toString + ")"
     }
 
-  def bash_command(command: String): String =
+  def bash_script(script: String): String =
     root match {
-      case None => command
+      case None => script
       case Some(msys_root) =>
         File.bash_path(msys_root + Path.explode("usr/bin/bash")) +
-          " -c " + Bash.string(MinGW.environment_prefix + command)
+          " -c " + Bash.string(MinGW.environment_export + script)
     }
 
   def get_root: Path =
@@ -47,7 +44,7 @@
   {
     if (Platform.is_windows) {
       get_root
-      try { require(Isabelle_System.bash(bash_command("uname -s")).check.out.startsWith("MSYS")) }
+      try { require(Isabelle_System.bash(bash_script("uname -s")).check.out.startsWith("MSYS")) }
       catch { case ERROR(_) => error("Bad msys/mingw installation " + get_root) }
     }
   }