Admin/rsync-isabelle

--- a/Admin/rsync-isabelle	Tue Mar 21 15:26:21 2000 +0100
+++ b/Admin/rsync-isabelle	Tue Mar 21 15:32:08 2000 +0100
@@ -111,6 +111,7 @@
   exit 0
 fi
 
+
 # arguments
 
 [ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }