diff -r 233dd3bb2390 -r 908f6776a59b Admin/isatest-makeall
--- a/Admin/isatest-makeall	Mon May 05 18:36:00 2003 +0200
+++ b/Admin/isatest-makeall	Tue May 06 09:23:13 2003 +0200
@@ -7,16 +7,19 @@
 # DESCRIPTION: Run isatool makeall from specified distribution and settings.
 #              Send email if it fails.
 
+# canoncical home for all platforms
+HOME=/usr/stud/isatest
+
 ## global settings
 MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
 
-LOGPREFIX=~/log
+LOGPREFIX=$HOME/log
 
 MASTERLOG=$LOGPREFIX/isatest.log
 
 TMP=/tmp/isatest-makeall.$$
 
-MAIL=~/bin/pmail
+MAIL=$HOME/bin/pmail
 
 ## diagnostics
 
@@ -107,7 +110,7 @@
     then
         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
         gzip -f $TESTLOG
-	rm -rf ~/isabelle-$SHORT
+	rm -rf $HOME/isabelle-$SHORT
     else
         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
 	FAIL="$FAIL$SHORT "