Admin/polyml/settings
changeset 51060 9effce0ce1e1
parent 49598 7bc5fcc03564
child 53686 432edb1a2469
--- 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
     ;;
   *)