equal
deleted
inserted
replaced
83 echo -n "Building $ITEM ... " |
83 echo -n "Building $ITEM ... " |
84 LOG="$LOGDIR/$ITEM" |
84 LOG="$LOGDIR/$ITEM" |
85 |
85 |
86 $ISABELLE \ |
86 $ISABELLE \ |
87 -e "val ml_system = \"$ML_SYSTEM\";" \ |
87 -e "val ml_system = \"$ML_SYSTEM\";" \ |
88 -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \ |
88 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ |
89 -q -w RAW_ML_SYSTEM Pure > $LOG 2>&1 |
89 -q -w RAW_ML_SYSTEM Pure > $LOG 2>&1 |
90 else |
90 else |
91 ITEM="RAW" |
91 ITEM="RAW" |
92 echo -n "Building $ITEM ... " |
92 echo -n "Building $ITEM ... " |
93 LOG="$LOGDIR/$ITEM" |
93 LOG="$LOGDIR/$ITEM" |
94 |
94 |
95 $ISABELLE \ |
95 $ISABELLE \ |
96 -e "val ml_system = \"$ML_SYSTEM\";" \ |
96 -e "val ml_system = \"$ML_SYSTEM\";" \ |
97 -e "use\"$COMPAT\";" \ |
97 -e "use\"$COMPAT\" handle _ => exit 1;;" \ |
98 -q -w RAW_ML_SYSTEM RAW > $LOG 2>&1 |
98 -q -w RAW_ML_SYSTEM RAW > $LOG 2>&1 |
99 fi |
99 fi |
100 |
100 |
101 RC=$? |
101 RC=$? |
102 |
102 |