Admin/mirror-dist
changeset 8347 8927067ef107
parent 8346 562090b1f128
child 8396 16f6de8c897b
     1.1 --- a/Admin/mirror-dist	Mon Mar 06 15:24:07 2000 +0100
     1.2 +++ b/Admin/mirror-dist	Mon Mar 06 15:44:51 2000 +0100
     1.3 @@ -20,5 +20,4 @@
     1.4      ;;
     1.5  esac
     1.6  
     1.7 -rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
     1.8 -  rsync://sunbroy30.informatik.tu-muenchen.de:8730/isabelle-dist/. $DEST/.
     1.9 +rsync -va --delete rsync://www4.in.tum.de:8730/isabelle-dist/. $DEST/.