# HG changeset patch
# User wenzelm
# Date 1602360347 -7200
# Node ID b8b97c49e3392857b598cee16f8ca3ddd2fc1a85
# Parent  8e38c8405788f35b498135d595a803b2fe6d5d38
tuned signature;

diff -r 8e38c8405788 -r b8b97c49e339 src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala	Sat Oct 10 22:04:51 2020 +0200
+++ b/src/Pure/Admin/build_csdp.scala	Sat Oct 10 22:05:47 2020 +0200
@@ -201,7 +201,7 @@
   Build prover component from official downloads.
 """,
         "D:" -> (arg => target_dir = Path.explode(arg)),
-        "M:" -> (arg => mingw = MinGW.root(Path.explode(arg))),
+        "M:" -> (arg => mingw = MinGW(Path.explode(arg))),
         "U:" -> (arg => download_url = arg),
         "v" -> (_ => verbose = true))
 
diff -r 8e38c8405788 -r b8b97c49e339 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Sat Oct 10 22:04:51 2020 +0200
+++ b/src/Pure/Admin/build_polyml.scala	Sat Oct 10 22:05:47 2020 +0200
@@ -255,7 +255,7 @@
   Build Poly/ML in the ROOT directory of its sources, with additional
   CONFIGURE_OPTIONS (e.g. --without-gmp).
 """,
-        "M:" -> (arg => mingw = MinGW.root(Path.explode(arg))),
+        "M:" -> (arg => mingw = MinGW(Path.explode(arg))),
         "m:" ->
           {
             case "32" => arch_64 = false
diff -r 8e38c8405788 -r b8b97c49e339 src/Pure/System/mingw.scala
--- a/src/Pure/System/mingw.scala	Sat Oct 10 22:04:51 2020 +0200
+++ b/src/Pure/System/mingw.scala	Sat Oct 10 22:05:47 2020 +0200
@@ -16,7 +16,7 @@
     environment.map(a => "export " + Bash.string(a)).mkString("", "\n", "\n")
 
   val none: MinGW = new MinGW(None)
-  def root(path: Path) = new MinGW(Some(path))
+  def apply(path: Path) = new MinGW(Some(path))
 }
 
 class MinGW private(val root: Option[Path])
@@ -24,7 +24,7 @@
   override def toString: String =
     root match {
       case None => "MinGW.none"
-      case Some(msys_root) => "MinGW.root(" + msys_root.toString + ")"
+      case Some(msys_root) => "MinGW(" + msys_root.toString + ")"
     }
 
   def bash_script(script: String): String =