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';
wenzelm@8222
     1
#!/bin/bash
wenzelm@8222
     2
#
wenzelm@8222
     3
# $Id$
wenzelm@8222
     4
#
wenzelm@8222
     5
wenzelm@8321
     6
HOST=$(hostname)
wenzelm@8321
     7
wenzelm@8321
     8
case ${HOST} in
kleing@9286
     9
  sunbroy51)
wenzelm@8222
    10
    DEST=/home/html/isabelle/html-data
wenzelm@8222
    11
    ;;
paulson@8225
    12
  *.cl.cam.ac.uk)
paulson@8225
    13
    USER=paulson
paulson@8225
    14
    DEST=/anfs/www/html/Research/HVG/Isabelle
wenzelm@8222
    15
    ;;
wenzelm@8222
    16
  *)
wenzelm@8321
    17
    echo "Unknown destination directory for ${HOST}"
wenzelm@8222
    18
    exit 2
wenzelm@8222
    19
    ;;
wenzelm@8222
    20
esac
wenzelm@8222
    21
wenzelm@8222
    22
rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
paulson@8225
    23
  $USER@sunbroy1.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/www/. $DEST/.