# HG changeset patch # User wenzelm # Date 953649128 -3600 # Node ID dc053bc2ea06731b21f3e3c331bc401f9d26663b # Parent 263a30b90c164cd353d761fef3da42cfa7922224 tuned; diff -r 263a30b90c16 -r dc053bc2ea06 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; }