equal
deleted
inserted
replaced
1 #!/bin/bash |
1 #!/bin/bash |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # |
4 # |
5 |
5 |
6 case $(hostname) in |
6 HOST=$(hostname) |
|
7 |
|
8 case ${HOST} in |
7 sunbroy30) |
9 sunbroy30) |
8 DEST=/home/html/isabelle/html-data |
10 DEST=/home/html/isabelle/html-data |
9 ;; |
11 ;; |
10 *.cl.cam.ac.uk) |
12 *.cl.cam.ac.uk) |
11 USER=paulson |
13 USER=paulson |
12 DEST=/anfs/www/html/Research/HVG/Isabelle |
14 DEST=/anfs/www/html/Research/HVG/Isabelle |
13 ;; |
15 ;; |
14 *) |
16 *) |
15 echo "Unknown destination directory for $(hostname)!" |
17 echo "Unknown destination directory for ${HOST}" |
16 exit 2 |
18 exit 2 |
17 ;; |
19 ;; |
18 esac |
20 esac |
19 |
21 |
20 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \ |
22 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \ |