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 foobar) |
7 |
8 DEST=/foo/bar/dist |
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 |
9 ;; |
15 ;; |
10 *) |
16 *) |
11 echo "Unknown destination directory!" |
17 echo "Unknown destination directory for ${HOST}" |
12 exit 2 |
18 exit 2 |
13 ;; |
19 ;; |
14 esac |
20 esac |
15 |
21 |
16 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \ |
22 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \ |
17 sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/. |
23 $USER@sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/. |