1.1 --- a/Admin/isasync	Sat Nov 19 14:22:28 2005 +0100
     1.2 +++ b/Admin/isasync	Mon Nov 21 10:44:14 2005 +0100
     1.3 @@ -128,4 +128,4 @@
     1.4  
     1.5  ## main
     1.6  
     1.7 -exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC/." "$DEST/."
     1.8 +exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC" "$DEST/"