--- a/Admin/mirror-dist Tue Nov 28 01:11:12 2000 +0100 +++ b/Admin/mirror-dist Tue Nov 28 01:22:56 2000 +0100 @@ -5,7 +5,7 @@ HOST=$(hostname) -case ${HOST} in +case ${HOST} in sunbroy*) #test DEST=/tmp/isabelle-dist