diff -r 38b111451155 -r e1b85512d87d src/Pure/mk
--- a/src/Pure/mk	Tue May 31 11:53:21 2005 +0200
+++ b/src/Pure/mk	Tue May 31 11:53:22 2005 +0200
@@ -65,8 +65,7 @@
 # get compatibility file
 
 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
-[ -z "$ML_SYSTEM" ] && \
-  fail "Missing ML system settings! Probably not run via 'isatool make'."
+[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
 
 COMPAT=""
 [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"