changeset 28982 | 75f221d67515 |
parent 28597 | e76e7b96a517 |
child 31496 | c4b74075fc17 |
--- a/Admin/isatest/isatest-makeall Thu Dec 04 09:12:41 2008 -0800 +++ b/Admin/isatest/isatest-makeall Fri Dec 05 11:33:03 2008 +1100 @@ -133,6 +133,11 @@ echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 + if [ "${ISABELLE_HOME_USER:0:14}" == "/tmp/isabelle-" ]; then + echo "--- cleaning up old $ISABELLE_HOME_USER" + rm -rf $ISABELLE_HOME_USER + fi + cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings (ulimit -t $MAXTIME; cd $DIR; $NICE $TOOL >> $TESTLOG 2>&1)