# HG changeset patch
# User wenzelm
# Date 952353891 -3600
# Node ID 8927067ef10755e926924997916fb8ff00a34c61
# Parent  562090b1f1285a06accccaed9364e842805fbe37
rsyncd setup;
--delete mode (beware!);

diff -r 562090b1f128 -r 8927067ef107 Admin/mirror-dist
--- a/Admin/mirror-dist	Mon Mar 06 15:24:07 2000 +0100
+++ b/Admin/mirror-dist	Mon Mar 06 15:44:51 2000 +0100
@@ -20,5 +20,4 @@
     ;;
 esac
 
-rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
-  rsync://sunbroy30.informatik.tu-muenchen.de:8730/isabelle-dist/. $DEST/.
+rsync -va --delete rsync://www4.in.tum.de:8730/isabelle-dist/. $DEST/.