equal
deleted
inserted
replaced
47 |
47 |
48 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
48 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
49 [ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!" |
49 [ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!" |
50 |
50 |
51 COMPAT="" |
51 COMPAT="" |
52 [ -f "RAW/${ML_SYSTEM_BASE}.ML" ] && COMPAT="RAW/${ML_SYSTEM_BASE}.ML" |
52 [ -f "RAW/ROOT_${ML_SYSTEM_BASE}.ML" ] && COMPAT="RAW/ROOT_${ML_SYSTEM_BASE}.ML" |
53 [ -f "RAW/${ML_SYSTEM}.ML" ] && COMPAT="RAW/${ML_SYSTEM}.ML" |
53 [ -f "RAW/ROOT_${ML_SYSTEM}.ML" ] && COMPAT="RAW/ROOT_${ML_SYSTEM}.ML" |
54 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!" |
54 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!" |
55 |
55 |
56 |
56 |
57 # run isabelle |
57 # run isabelle |
58 |
58 |