# HG changeset patch
# User wenzelm
# Date 850726808 -3600
# Node ID 0293bc1cecfc07c90af6a4caa4d57de75a28bb8f
# Parent  4b08766bc9d1f01ea247ba389ae34428850d0130
now passes ML_SYSTEM as ml_system;

diff -r 4b08766bc9d1 -r 0293bc1cecfc src/Pure/mk
--- a/src/Pure/mk	Mon Dec 16 09:59:18 1996 +0100
+++ b/src/Pure/mk	Mon Dec 16 10:00:08 1996 +0100
@@ -30,4 +30,7 @@
 [ -f "ML-Systems/$ML_SYSTEM.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM.ML"
 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
 
-exec isabelle -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" -cq SYSTEM Pure
+exec isabelle \
+  -e "val ml_system = \"$ML_SYSTEM\";" \
+  -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
+  -cq SYSTEM Pure