Admin/isatest/isatest-makeall
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)