| changeset 6186 | 72abe86d9418 |
| parent 4495 | 8648ba842d14 |
| child 6239 | 6b9194aff620 |
--- a/src/Pure/mk Wed Feb 03 16:40:42 1999 +0100 +++ b/src/Pure/mk Wed Feb 03 16:41:00 1999 +0100 @@ -60,7 +60,7 @@ ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-) [ -z "$ML_SYSTEM" ] && \ - fail "Missing ML system settings! Probably not run via 'isatool make'?." + fail "Missing ML system settings! Probably not run via 'isatool make'." COMPAT="" [ -f "ML-Systems/$ML_SYSTEM_BASE.ML" ] && COMPAT="ML-Systems/$ML_SYSTEM_BASE.ML"