# HG changeset patch
# User kleing
# Date 952352647 -3600
# Node ID 562090b1f1285a06accccaed9364e842805fbe37
# Parent  e708af969264707de8d430dd4aacd8edc8f01305
switched to mirroring with rsync server

diff -r e708af969264 -r 562090b1f128 Admin/mirror-dist
--- a/Admin/mirror-dist	Mon Mar 06 12:04:39 2000 +0100
+++ b/Admin/mirror-dist	Mon Mar 06 15:24:07 2000 +0100
@@ -12,7 +12,6 @@
     mkdir -p $DEST
     ;;
   *.cl.cam.ac.uk)
-    USER=paulson
     DEST=/anfs/www/html/Research/HVG/Isabelle/dist
     ;;
   *)
@@ -22,4 +21,4 @@
 esac
 
 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
-  $USER@sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/.
+  rsync://sunbroy30.informatik.tu-muenchen.de:8730/isabelle-dist/. $DEST/.
diff -r e708af969264 -r 562090b1f128 Admin/rsyncd
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/rsyncd	Mon Mar 06 15:24:07 2000 +0100
@@ -0,0 +1,9 @@
+#!/bin/bash
+#
+# rsync server start script
+#
+# $Id$
+#
+
+rsync --daemon --config=/usr/proj/isabelle/rsyncd.conf --port=8730
+
diff -r e708af969264 -r 562090b1f128 Admin/rsyncd.conf
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/rsyncd.conf	Mon Mar 06 15:24:07 2000 +0100
@@ -0,0 +1,16 @@
+#
+# rsync server configuration
+#
+# $Id$
+#
+
+uid = nobody 
+gid = nobody 
+use chroot = no 
+log file = /usr/proj/isabelle/rsyncd.log
+read only = true
+
+[isabelle-dist]
+        path = /home/html/isabelle/html-data/dist/
+        comment = Isabelle distribution area
+