# HG changeset patch
# User wenzelm
# Date 1518526717 -3600
# Node ID 738b4d4eeb6187a31864325884f960b721649c5e
# Parent  1b2be3666b8917c21a63dc8c4d8bf5d65b4b0e28
no --enable-shared: leads to slow bigint operations (e.g. in session HOL-ODE-Examples);

diff -r 1b2be3666b89 -r 738b4d4eeb61 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Tue Feb 13 12:18:16 2018 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Tue Feb 13 13:58:37 2018 +0100
@@ -28,11 +28,11 @@
       Platform_Info(
         options_multilib =
           List("--build=i386", "CFLAGS=-m32 -O3", "CXXFLAGS=-m32 -O3", "CCASFLAGS=-m32",
-            "LDFLAGS=-Wl,-rpath,_DUMMY_", "--enable-shared", "--without-gmp"),
-        options = List("LDFLAGS=-Wl,-rpath,_DUMMY_", "--enable-shared")),
+            "LDFLAGS=-Wl,-rpath,_DUMMY_", "--without-gmp"),
+        options = List("LDFLAGS=-Wl,-rpath,_DUMMY_")),
     "x86_64-linux" ->
       Platform_Info(
-        options = List("LDFLAGS=-Wl,-rpath,_DUMMY_", "--enable-shared")),
+        options = List("LDFLAGS=-Wl,-rpath,_DUMMY_")),
     "x86-darwin" ->
       Platform_Info(
         options =