| changeset 8347 | 8927067ef107 |
| parent 8346 | 562090b1f128 |
| child 8396 | 16f6de8c897b |
--- 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/.