# HG changeset patch
# User wenzelm
# Date 1518349883 -3600
# Node ID 5efb88c90051a92b3200636565b7398b075370da
# Parent  66253039d5caabbf6437e1f1a5e72e5fcb89ddb4
clarified command-line defaults;

diff -r 66253039d5ca -r 5efb88c90051 Admin/polyml/README
--- a/Admin/polyml/README	Sun Feb 11 12:40:05 2018 +0100
+++ b/Admin/polyml/README	Sun Feb 11 12:51:23 2018 +0100
@@ -9,25 +9,28 @@
 
 * Linux:
 
-  $ isabelle build_polyml -m32 -s sha1 src --with-gmp
-  $ isabelle build_polyml -m64 -s sha1 src --with-gmp
+  $ isabelle build_polyml -m32 -s sha1 src
+  $ isabelle build_polyml -m64 -s sha1 src
 
 * Windows (Cygwin shell)
 
-  $ isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src --with-gmp
-  $ isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src --with-gmp
+  $ isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src
+  $ isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src
 
 * Mac OS X:
 
-  $ isabelle build_polyml -m32 -s sha1 src --with-gmp
-  $ isabelle build_polyml -m64 -s sha1 src --with-gmp
+  $ isabelle build_polyml -m32 -s sha1 src
+  $ isabelle build_polyml -m64 -s sha1 src
 
 
 Building libgmp on Mac OS X
 ===========================
 
-The GNU Multiple Precision Arithmetic Library is not included in Mac OS X
-by default, but it can be built from sources as follows.
+The build_polyml invocations above implicitly use the GNU Multiple Precision
+Arithmetic Library (libgmp), but that is not available on Mac OS X by default.
+Appending "--without-gmp" to the command-line omits this library. Building
+libgmp properly works as follows (library headers and binaries will be placed
+in /usr/local).
 
 * Download:
 
@@ -50,4 +53,4 @@
 
 
         Makarius
-        10-Feb-2018
+        11-Feb-2018
diff -r 66253039d5ca -r 5efb88c90051 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Sun Feb 11 12:40:05 2018 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Sun Feb 11 12:51:23 2018 +0100
@@ -112,7 +112,8 @@
     val configure_options =
       (if (!arch_64 && Isabelle_System.getenv("ISABELLE_PLATFORM64") == "x86_64-linux")
         info.options_multilib
-       else info.options) ::: List("--enable-shared", "--enable-intinf-as-int") ::: options
+       else info.options) :::
+      List("--enable-shared", "--enable-intinf-as-int", "--with-gmp") ::: options
 
     bash(root,
       info.setup + "\n" +
@@ -248,7 +249,7 @@
     -s DIR       sha1 sources, see https://bitbucket.org/isabelle_project/sha1
 
   Build Poly/ML in the ROOT directory of its sources, with additional
-  CONFIGURE_OPTIONS (e.g. --with-gmp).
+  CONFIGURE_OPTIONS (e.g. --without-gmp).
 """,
           "M:" -> (arg => msys_root = Some(Path.explode(arg))),
           "m:" ->