equal
deleted
inserted
replaced
119 DEST="$1"; shift; |
119 DEST="$1"; shift; |
120 |
120 |
121 |
121 |
122 ## main |
122 ## main |
123 |
123 |
124 exec rsync -vaL $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/." |
124 exec rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/." |