Admin/mirror-dist
changeset 8322 6ba8356baa34
parent 8224 97e26127fb6b
child 8323 64b67ed25a59
     1.1 --- a/Admin/mirror-dist	Wed Mar 01 16:38:59 2000 +0100
     1.2 +++ b/Admin/mirror-dist	Wed Mar 01 16:39:17 2000 +0100
     1.3 @@ -3,15 +3,21 @@
     1.4  # $Id$
     1.5  #
     1.6  
     1.7 -case $(hostname) in
     1.8 -  foobar)
     1.9 -    DEST=/foo/bar/dist
    1.10 +HOST=$(hostname)
    1.11 +
    1.12 +case  ${HOST} in
    1.13 +  *.cl.cam.ac.uk)
    1.14 +    USER=paulson
    1.15 +    DEST=/anfs/www/html/Research/HVG/Isabelle/dist
    1.16 +    ;;
    1.17 +  sunbroy79)
    1.18 +    DEST=/tmp/isabelle-dist
    1.19      ;;
    1.20    *)
    1.21 -    echo "Unknown destination directory!"
    1.22 +    echo "Unknown destination directory for ${HOST}"
    1.23      exit 2
    1.24      ;;
    1.25  esac
    1.26  
    1.27  rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
    1.28 -  sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/.
    1.29 +  $USER@sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/.