no --enable-shared: leads to slow bigint operations (e.g. in session HOL-ODE-Examples);
authorwenzelm
Tue, 13 Feb 2018 13:58:37 +0100
changeset 67609 738b4d4eeb61
parent 67608 1b2be3666b89
child 67610 4939494ed791
no --enable-shared: leads to slow bigint operations (e.g. in session HOL-ODE-Examples);
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 =