--- 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
--- 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/."