equal
deleted
inserted
replaced
28 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!" |
28 [ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!" |
29 |
29 |
30 $ISABELLE \ |
30 $ISABELLE \ |
31 -e "val ml_system = \"$ML_SYSTEM\";" \ |
31 -e "val ml_system = \"$ML_SYSTEM\";" \ |
32 -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \ |
32 -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \ |
33 -q RAW_ML_SYSTEM Pure |
33 -q -w RAW_ML_SYSTEM Pure |
34 |
|
35 chmod -w $ISABELLE_OUTPUT/Pure |
|