Admin/mirror-main
author paulson
Thu, 10 Feb 2000 11:03:54 +0100
changeset 8225 fc5db20d7f6f
parent 8222 55fed562d8ed
child 8321 dc13f558856d
permissions -rwxr-xr-x
Cambridge-specific modifications
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8222
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
     1
#!/bin/bash
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
     2
#
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
     3
# $Id$
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
     4
#
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
     5
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
     6
case $(hostname) in
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
     7
  sunbroy30)
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
     8
    DEST=/home/html/isabelle/html-data
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
     9
    ;;
8225
fc5db20d7f6f Cambridge-specific modifications
paulson
parents: 8222
diff changeset
    10
  *.cl.cam.ac.uk)
fc5db20d7f6f Cambridge-specific modifications
paulson
parents: 8222
diff changeset
    11
    USER=paulson
fc5db20d7f6f Cambridge-specific modifications
paulson
parents: 8222
diff changeset
    12
    DEST=/anfs/www/html/Research/HVG/Isabelle
8222
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
    13
    ;;
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
    14
  *)
8225
fc5db20d7f6f Cambridge-specific modifications
paulson
parents: 8222
diff changeset
    15
    echo "Unknown destination directory for $(hostname)!"
8222
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
    16
    exit 2
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
    17
    ;;
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
    18
esac
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
    19
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset
    20
rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
8225
fc5db20d7f6f Cambridge-specific modifications
paulson
parents: 8222
diff changeset
    21
  $USER@sunbroy1.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/www/. $DEST/.