Admin/mirror-dist
changeset 8347 8927067ef107
parent 8346 562090b1f128
child 8396 16f6de8c897b
equal deleted inserted replaced
8346:562090b1f128 8347:8927067ef107
    18     echo "Unknown destination directory for ${HOST}"
    18     echo "Unknown destination directory for ${HOST}"
    19     exit 2
    19     exit 2
    20     ;;
    20     ;;
    21 esac
    21 esac
    22 
    22 
    23 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
    23 rsync -va --delete rsync://www4.in.tum.de:8730/isabelle-dist/. $DEST/.
    24   rsync://sunbroy30.informatik.tu-muenchen.de:8730/isabelle-dist/. $DEST/.