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