# HG changeset patch
# User wenzelm
# Date 1744311242 -7200
# Node ID 041d65893a85830043d74e11370dc4c02b3a81cc
# Parent  489f4a79d2158f542f7949949fd41afd01020227
clarified GMP build options, notably for Windows;

diff -r 489f4a79d215 -r 041d65893a85 src/Pure/Admin/component_polyml.scala
--- a/src/Pure/Admin/component_polyml.scala	Thu Apr 10 20:39:06 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala	Thu Apr 10 20:54:02 2025 +0200
@@ -81,7 +81,8 @@
     progress.echo("Building GMP library ...")
     platform_context.execute(root,
       "[ -f Makefile ] && make distclean",
-      "./configure --enable-cxx --build=" + platform_arch + "-" + platform_os +
+      "./configure --disable-static --enable-shared --enable-cxx" +
+        " --build=" + platform_arch + "-" + platform_os +
         " --prefix=" + Bash.string(platform_context.standard_path(target_dir)) +
         if_proper(options, " " + Bash.strings(options)),
       "make",