diff -r 6ba8356baa34 -r 64b67ed25a59 Admin/mirror-dist
--- a/Admin/mirror-dist	Wed Mar 01 16:39:17 2000 +0100
+++ b/Admin/mirror-dist	Wed Mar 01 16:40:14 2000 +0100
@@ -6,13 +6,15 @@
 HOST=$(hostname)
 
 case  ${HOST} in
+  sunbroy79)
+    #test
+    DEST=/tmp/isabelle-dist
+    mkdir -p $DEST
+    ;;
   *.cl.cam.ac.uk)
     USER=paulson
     DEST=/anfs/www/html/Research/HVG/Isabelle/dist
     ;;
-  sunbroy79)
-    DEST=/tmp/isabelle-dist
-    ;;
   *)
     echo "Unknown destination directory for ${HOST}"
     exit 2