diff -r 3bdebf6ad9da -r 0cebcbeac4c7 Admin/polyml/settings
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/polyml/settings	Wed Aug 29 20:16:22 2012 +0200
@@ -0,0 +1,43 @@
+# -*- shell-script -*- :mode=shellscript:
+
+# basic settings
+
+#ML_SYSTEM=polyml-5.4.1
+#ML_PLATFORM="$ISABELLE_PLATFORM"
+#ML_HOME="$COMPONENT/$ML_PLATFORM"
+#ML_OPTIONS="-H 500"
+#ML_SOURCES="$ML_HOME/../src"
+
+
+# smart settings
+
+ML_SYSTEM=polyml-5.4.1
+
+case "$ISABELLE_PLATFORM" in
+  *-linux)
+    if env LD_LIBRARY_PATH="$COMPONENT/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \
+      "$COMPONENT/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null
+    then
+      ML_PLATFORM="$ISABELLE_PLATFORM32"
+    else
+      echo >&2 "### Cannot execute Poly/ML in 32bit mode -- using bulky 64bit version instead"
+      ML_PLATFORM="$ISABELLE_PLATFORM64"
+    fi
+    ;;
+  *)
+    ML_PLATFORM="$ISABELLE_PLATFORM32"
+    ;;
+esac
+
+case "$ML_PLATFORM" in
+  x86_64-*)
+    ML_OPTIONS="-H 1000"
+    ;;
+  *)
+    ML_OPTIONS="-H 500"
+    ;;
+esac
+
+ML_HOME="$COMPONENT/$ML_PLATFORM"
+ML_SOURCES="$COMPONENT/src"
+