no --enable-shared: leads to slow bigint operations (e.g. in session HOL-ODE-Examples);
--- 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 =