equal
deleted
inserted
replaced
23 echo "Unknown destination directory for ${HOST}" |
23 echo "Unknown destination directory for ${HOST}" |
24 exit 2 |
24 exit 2 |
25 ;; |
25 ;; |
26 esac |
26 esac |
27 |
27 |
28 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \ |
28 echo "Warning: this script now mirrors the *complete* Isabelle site" |
|
29 |
|
30 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va --copy-links \ |
29 $USER@sunbroy2.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/www/. $DEST/. |
31 $USER@sunbroy2.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/www/. $DEST/. |