changeset 16131 | e1b85512d87d |
parent 15790 | e68dab670fc5 |
child 16376 | 65e2df6d8e10 |
--- 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"