Admin/mirror-dist
changeset 8397 f2d371bde3c4
parent 8396 16f6de8c897b
child 8398 f1c80ed70f48
--- 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