diff -r 1add21f7cabc -r e8ae72c26025 src/Pure/build --- 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\"!"