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