# HG changeset patch
# User wenzelm
# Date 952619128 -3600
# Node ID f2d371bde3c40bd5172ac09ce9ea4680042c9db3
# Parent  16f6de8c897bd3fd58811fd7c8f75669ac409ce1
tuned;

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
diff -r 16f6de8c897b -r f2d371bde3c4 Admin/mirror-isabelle-dist
--- a/Admin/mirror-isabelle-dist	Thu Mar 09 17:19:49 2000 +0100
+++ b/Admin/mirror-isabelle-dist	Thu Mar 09 17:25:28 2000 +0100
@@ -5,23 +5,10 @@
 # $Id$
 #
 
-
-
-## self references
+## diagnostics
 
 PRG=`basename "$0"`
 
-if [ -h "$0" ]; then
-  THIS=`cd \`dirname "$0"\`; cd \`dirname \\\`find "$0" -ls | cut -d ">" -f 2\\\`\`; pwd`
-else
-  THIS=`cd \`dirname "$0"\`; pwd`
-fi
-
-SUPER=`cd "$THIS/.."; pwd`
-
-
-## diagnostics
-
 usage()
 {
   echo
@@ -29,7 +16,7 @@
   echo
   echo "  Options are:"
   echo "    -n    dry run, don't do anything, just report what would happen"
-  echo "    -d    delete files that are not on the server"
+  echo "    -d    delete files that are not on the server (beware!)"
   echo
   exit 1
 }
@@ -71,6 +58,7 @@
 
 DEST="$1"; shift;
 
+
 ## main
 
-rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. $DEST/.
\ No newline at end of file
+exec rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/."