# HG changeset patch
# User wenzelm
# Date 1518351878 -3600
# Node ID 6f819a5b4a92bc21c99b7f02ee9fe22c2de4c385
# Parent  5b4dd7a5b8828ec257da025ce716fa8c69302b6c
back to --disable-shared on windows to avoid odd core-dump of polyimport;

diff -r 5b4dd7a5b882 -r 6f819a5b4a92 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Sun Feb 11 13:13:03 2018 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Sun Feb 11 13:24:38 2018 +0100
@@ -45,7 +45,8 @@
     "x86-windows" ->
       Platform_Info(
         options =
-          List("--host=i686-w32-mingw32", "CPPFLAGS=-I/mingw32/include", "--disable-windows-gui"),
+          List("--host=i686-w32-mingw32", "CPPFLAGS=-I/mingw32/include",
+            "--disable-windows-gui", "--disable-shared"),
         setup =
           """PATH=/usr/bin:/bin:/mingw32/bin
             export CONFIG_SITE=/etc/config.site""",
@@ -56,7 +57,8 @@
     "x86_64-windows" ->
       Platform_Info(
         options =
-          List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
+          List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include",
+            "--disable-windows-gui", "--disable-shared"),
         setup =
           """PATH=/usr/bin:/bin:/mingw64/bin
             export CONFIG_SITE=/etc/config.site""",