equal
deleted
inserted
replaced
107 touch $RUNNING/$SHORT.running |
107 touch $RUNNING/$SHORT.running |
108 |
108 |
109 echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 |
109 echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 |
110 |
110 |
111 cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
111 cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
112 cd $DISTPREFIX/Isabelle/src/Pure |
|
113 $DISTPREFIX/Isabelle/bin/isatool make Pure $MFLAGS all >> $TESTLOG 2>&1 |
|
114 cd - |
|
115 $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 |
112 $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 |
116 |
113 |
117 if [ $? -eq 0 ] |
114 if [ $? -eq 0 ] |
118 then |
115 then |
119 # test log and cleanup |
116 # test log and cleanup |