diff -r c22ee06ac1a7 -r 857444b28267 Admin/isasync
--- 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/"