equal
deleted
inserted
replaced
89 LOG="$LOGDIR/$ITEM" |
89 LOG="$LOGDIR/$ITEM" |
90 |
90 |
91 "$ISABELLE" $COPY \ |
91 "$ISABELLE" $COPY \ |
92 -e "val ml_system = \"$ML_SYSTEM\";" \ |
92 -e "val ml_system = \"$ML_SYSTEM\";" \ |
93 -e "val ml_platform = \"$ML_PLATFORM\";" \ |
93 -e "val ml_platform = \"$ML_PLATFORM\";" \ |
94 -e "val share_data = NONE: ('a -> 'a) option;" \ |
|
95 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ |
94 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ |
96 -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 |
95 -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 |
97 RC="$?" |
96 RC="$?" |
98 else |
97 else |
99 ITEM="RAW" |
98 ITEM="RAW" |