Admin/mirror-main
author wenzelm
Fri Oct 12 12:08:04 2001 +0200 (2001-10-12)
changeset 11729 a7da2e8b5762
parent 9286 4ccadbdbbd24
child 12721 226fc0e2e7e3
permissions -rwxr-xr-x
removed read_inst', no longer export insts';
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 
     6 HOST=$(hostname)
     7 
     8 case ${HOST} in
     9   sunbroy51)
    10     DEST=/home/html/isabelle/html-data
    11     ;;
    12   *.cl.cam.ac.uk)
    13     USER=paulson
    14     DEST=/anfs/www/html/Research/HVG/Isabelle
    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@sunbroy1.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/www/. $DEST/.