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