# HG changeset patch
# User wenzelm
# Date 1744466456 -7200
# Node ID 5df2050f1c312ba53a3e755ce8d270a16b90a22a
# Parent  b52e57ed7e29ad0a1dcadb53ebbdb408cd15a06f
clarified default options: prefer GMP from source;

diff -r b52e57ed7e29 -r 5df2050f1c31 src/Pure/Admin/component_polyml.scala
--- a/src/Pure/Admin/component_polyml.scala	Fri Apr 11 22:17:06 2025 +0100
+++ b/src/Pure/Admin/component_polyml.scala	Sat Apr 12 16:00:56 2025 +0200
@@ -218,7 +218,9 @@
 
   /** skeleton for component **/
 
-  val standard_gmp_url = "https://gmplib.org/download/gmp/gmp-6.3.0.tar.bz2"
+  def default_gmp_url: String =
+    if (Platform.is_windows) ""
+    else "https://gmplib.org/download/gmp/gmp-6.3.0.tar.bz2"
 
   val default_polyml_url = "https://github.com/polyml/polyml/archive"
   val default_polyml_version = "90c0dbb2514e"
@@ -382,11 +384,11 @@
 
 * Linux and macOS
 
-  $ isabelle component_polyml -G:
+  $ isabelle component_polyml
 
 * Windows (Cygwin shell)
 
-  $ isabelle component_polyml -G: -M /cygdrive/c/msys64
+  $ isabelle component_polyml -M /cygdrive/c/msys64
 
 
         Makarius
@@ -477,7 +479,7 @@
       Scala_Project.here,
       { args =>
         var target_dir = Path.current
-        var gmp_url = ""
+        var gmp_url = default_gmp_url
         var mingw = MinGW.none
         var component_name = ""
         var sha1_url = default_sha1_url
@@ -492,8 +494,8 @@
 
   Options are:
     -D DIR       target directory (default ".")
-    -G URL       build GMP library from source: explicit URL or ":" for
-                 """ + standard_gmp_url + """
+    -G URL       GMP library source archive, or "" for none (--without-gmp)
+                 (default """ + quote(default_gmp_url) + """)
     -M DIR       msys/mingw root specification for Windows
     -N NAME      component name (default: derived from Poly/ML version)
     -S URL       SHA1 repository archive area
@@ -509,7 +511,7 @@
   CONFIGURE_OPTIONS.
 """,
           "D:" -> (arg => target_dir = Path.explode(arg)),
-          "G:" -> (arg => gmp_url = if (arg == ":") standard_gmp_url else arg),
+          "G:" -> (arg => gmp_url = arg),
           "M:" -> (arg => mingw = MinGW(Path.explode(arg))),
           "N:" -> (arg => component_name = arg),
           "S:" -> (arg => sha1_url = arg),