| changeset 8222 | 55fed562d8ed |
| child 8225 | fc5db20d7f6f |
| 8221:6be623684675 | 8222:55fed562d8ed |
|---|---|
1 #!/bin/bash |
|
2 # |
|
3 # $Id$ |
|
4 # |
|
5 |
|
6 case $(hostname) in |
|
7 sunbroy30) |
|
8 DEST=/home/html/isabelle/html-data |
|
9 ;; |
|
10 foobar) |
|
11 DEST=/foo/bar |
|
12 ;; |
|
13 *) |
|
14 echo "Unknown destination directory!" |
|
15 exit 2 |
|
16 ;; |
|
17 esac |
|
18 |
|
19 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \ |
|
20 sunbroy1.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/www/. $DEST/. |