diff -r 16f6de8c897b -r f2d371bde3c4 Admin/mirror-dist
--- a/Admin/mirror-dist	Thu Mar 09 17:19:49 2000 +0100
+++ b/Admin/mirror-dist	Thu Mar 09 17:25:28 2000 +0100
@@ -6,7 +6,7 @@
 HOST=$(hostname)
 
 case  ${HOST} in
-  sunbroy79)
+  sunbroy*)
     #test
     DEST=/tmp/isabelle-dist
     mkdir -p $DEST
@@ -20,4 +20,4 @@
     ;;
 esac
 
-mirror-isabelle-dist -d $DEST
+exec $(dirname $0)/mirror-isabelle-dist -d $DEST