--- a/Admin/mirror-dist Thu Mar 09 16:14:37 2000 +0100 +++ b/Admin/mirror-dist Thu Mar 09 17:19:49 2000 +0100 @@ -20,4 +20,4 @@ ;; esac -rsync -va --delete rsync://www4.in.tum.de:8730/isabelle-dist/. $DEST/. +mirror-isabelle-dist -d $DEST