tuned;
authorwenzelm
Tue Mar 21 15:32:08 2000 +0100 (2000-03-21)
changeset 8546dc053bc2ea06
parent 8545 263a30b90c16
child 8547 93b8685d004b
tuned;
Admin/rsync-isabelle
     1.1 --- a/Admin/rsync-isabelle	Tue Mar 21 15:26:21 2000 +0100
     1.2 +++ b/Admin/rsync-isabelle	Tue Mar 21 15:32:08 2000 +0100
     1.3 @@ -111,6 +111,7 @@
     1.4    exit 0
     1.5  fi
     1.6  
     1.7 +
     1.8  # arguments
     1.9  
    1.10  [ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }