Admin/mirror-dist
changeset 10531 a9e7786db49e
parent 8398 f1c80ed70f48
child 12721 226fc0e2e7e3
     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