src/Pure/build
changeset 62077 e8ae72c26025
parent 61925 ab52f183f020
child 62469 6d292ee30365
--- a/src/Pure/build	Wed Jan 06 10:08:09 2016 +0100
+++ b/src/Pure/build	Wed Jan 06 10:20:33 2016 +0100
@@ -49,8 +49,8 @@
 [ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
 
 COMPAT=""
-[ -f "RAW/${ML_SYSTEM_BASE}.ML" ] && COMPAT="RAW/${ML_SYSTEM_BASE}.ML"
-[ -f "RAW/${ML_SYSTEM}.ML" ] && COMPAT="RAW/${ML_SYSTEM}.ML"
+[ -f "RAW/ROOT_${ML_SYSTEM_BASE}.ML" ] && COMPAT="RAW/ROOT_${ML_SYSTEM_BASE}.ML"
+[ -f "RAW/ROOT_${ML_SYSTEM}.ML" ] && COMPAT="RAW/ROOT_${ML_SYSTEM}.ML"
 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"