--- 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; }