tuned;
authorwenzelm
Tue Nov 28 01:22:56 2000 +0100 (2000-11-28)
changeset 10531a9e7786db49e
parent 10530 df079a585e6d
child 10532 042f67eea015
tuned;
Admin/mirror-dist
     1.1 --- a/Admin/mirror-dist	Tue Nov 28 01:11:12 2000 +0100
     1.2 +++ b/Admin/mirror-dist	Tue Nov 28 01:22:56 2000 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  HOST=$(hostname)
     1.6  
     1.7 -case  ${HOST} in
     1.8 +case ${HOST} in
     1.9    sunbroy*)
    1.10      #test
    1.11      DEST=/tmp/isabelle-dist