# HG changeset patch # User haftmann # Date 1117972850 -7200 # Node ID 3d5256d3f3f44c3dbb2227c5b792e10b75bd59b6 # Parent bcf05183df9e4844bfe8b325e11acbc2371e6e90 added rsync symlink option diff -r bcf05183df9e -r 3d5256d3f3f4 Admin/rsync-isabelle --- a/Admin/rsync-isabelle Sun Jun 05 13:49:51 2005 +0200 +++ b/Admin/rsync-isabelle Sun Jun 05 14:00:50 2005 +0200 @@ -121,4 +121,4 @@ ## main -exec rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/." +exec rsync -vaL $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/."