Admin/mirror-dist
changeset 8323 64b67ed25a59
parent 8322 6ba8356baa34
child 8346 562090b1f128
     1.1 --- a/Admin/mirror-dist	Wed Mar 01 16:39:17 2000 +0100
     1.2 +++ b/Admin/mirror-dist	Wed Mar 01 16:40:14 2000 +0100
     1.3 @@ -6,13 +6,15 @@
     1.4  HOST=$(hostname)
     1.5  
     1.6  case  ${HOST} in
     1.7 +  sunbroy79)
     1.8 +    #test
     1.9 +    DEST=/tmp/isabelle-dist
    1.10 +    mkdir -p $DEST
    1.11 +    ;;
    1.12    *.cl.cam.ac.uk)
    1.13      USER=paulson
    1.14      DEST=/anfs/www/html/Research/HVG/Isabelle/dist
    1.15      ;;
    1.16 -  sunbroy79)
    1.17 -    DEST=/tmp/isabelle-dist
    1.18 -    ;;
    1.19    *)
    1.20      echo "Unknown destination directory for ${HOST}"
    1.21      exit 2