Admin/isasync
changeset 18214 857444b28267
parent 17728 1412f84c420a
child 25463 8b9c4582795a
equal deleted inserted replaced
18213:c22ee06ac1a7 18214:857444b28267
   126 DEST="$1"; shift;
   126 DEST="$1"; shift;
   127 
   127 
   128 
   128 
   129 ## main
   129 ## main
   130 
   130 
   131 exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC/." "$DEST/."
   131 exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC" "$DEST/"