# HG changeset patch
# User wenzelm
# Date 1359226369 -3600
# Node ID 9effce0ce1e168f60971fbbef607bea9883e1d58
# Parent  c6a74742f8fef906cb2539b49395e6b584cb4707
tuned ML platform fallback;

diff -r c6a74742f8fe -r 9effce0ce1e1 Admin/polyml/settings
--- a/Admin/polyml/settings	Sat Jan 26 16:51:43 2013 +0100
+++ b/Admin/polyml/settings	Sat Jan 26 19:52:49 2013 +0100
@@ -20,9 +20,12 @@
     then
       ML_PLATFORM="$ISABELLE_PLATFORM32"
     else
-      echo >&2 "### Cannot execute Poly/ML in 32bit mode: missing shared libraries for C/C++"
-      echo >&2 "### Using more voluminous 64bit version of Poly/ML instead"
       ML_PLATFORM="$ISABELLE_PLATFORM64"
+      if [ -z "$ML_PLATFORM_FALLBACK" ]; then
+        echo >&2 "### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)"
+        echo >&2 "### Using bulky 64bit version of Poly/ML instead"
+        ML_PLATFORM_FALLBACK="true"
+      fi
     fi
     ;;
   *)