equal
deleted
inserted
replaced
78 |
78 |
79 SECONDS=0 |
79 SECONDS=0 |
80 |
80 |
81 if [ -z "$RAW" ]; then |
81 if [ -z "$RAW" ]; then |
82 ITEM="Pure" |
82 ITEM="Pure" |
83 echo -n "Building $ITEM ..." |
83 echo "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 RC=$? |
90 RC=$? |
91 else |
91 else |
92 ITEM="RAW" |
92 ITEM="RAW" |
93 echo -n "Building $ITEM ..." |
93 echo "Building $ITEM ..." |
94 LOG="$LOGDIR/$ITEM" |
94 LOG="$LOGDIR/$ITEM" |
95 |
95 |
96 $ISABELLE \ |
96 $ISABELLE \ |
97 -e "val ml_system = \"$ML_SYSTEM\";" \ |
97 -e "val ml_system = \"$ML_SYSTEM\";" \ |
98 -e "use\"$COMPAT\" handle _ => exit 1;;" \ |
98 -e "use\"$COMPAT\" handle _ => exit 1;;" \ |
104 |
104 |
105 |
105 |
106 # exit status |
106 # exit status |
107 |
107 |
108 if [ $RC -eq 0 ]; then |
108 if [ $RC -eq 0 ]; then |
109 echo " OK ($ELAPSED elapsed time)" |
109 echo "Finished $ITEM ($ELAPSED elapsed time)" |
110 gzip --force "$LOG" |
110 gzip --force "$LOG" |
111 else |
111 else |
112 echo |
|
113 echo "$ITEM FAILED" |
112 echo "$ITEM FAILED" |
114 echo "(see also $LOG)" |
113 echo "(see also $LOG)" |
115 echo; tail $LOG; echo |
114 echo; tail $LOG; echo |
116 fi |
115 fi |
117 |
116 |