Admin/mirror-dist
author wenzelm
Wed Mar 01 16:39:17 2000 +0100 (2000-03-01)
changeset 8322 6ba8356baa34
parent 8224 97e26127fb6b
child 8323 64b67ed25a59
permissions -rwxr-xr-x
proper setup;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 
     6 HOST=$(hostname)
     7 
     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
    15     ;;
    16   *)
    17     echo "Unknown destination directory for ${HOST}"
    18     exit 2
    19     ;;
    20 esac
    21 
    22 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
    23   $USER@sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/.