Admin/mirror-dist
changeset 8322 6ba8356baa34
parent 8224 97e26127fb6b
child 8323 64b67ed25a59
equal deleted inserted replaced
8321:dc13f558856d 8322:6ba8356baa34
     1 #!/bin/bash
     1 #!/bin/bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
     4 #
     4 #
     5 
     5 
     6 case $(hostname) in
     6 HOST=$(hostname)
     7   foobar)
     7 
     8     DEST=/foo/bar/dist
     8 case  ${HOST} in
       
     9   *.cl.cam.ac.uk)
       
    10     USER=paulson
       
    11     DEST=/anfs/www/html/Research/HVG/Isabelle/dist
       
    12     ;;
       
    13   sunbroy79)
       
    14     DEST=/tmp/isabelle-dist
     9     ;;
    15     ;;
    10   *)
    16   *)
    11     echo "Unknown destination directory!"
    17     echo "Unknown destination directory for ${HOST}"
    12     exit 2
    18     exit 2
    13     ;;
    19     ;;
    14 esac
    20 esac
    15 
    21 
    16 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
    22 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
    17   sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/.
    23   $USER@sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/.