| changeset 48190 | 76b6207eb000 |
| parent 48189 | cd0a411b7fc1 |
| child 48191 | c1def7433a72 |
| child 48199 | 0e552737cc5a |
| 48189:cd0a411b7fc1 | 48190:76b6207eb000 |
|---|---|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # mirrors the Isabelle website |
|
4 |
|
5 HOST=$(hostname) |
|
6 |
|
7 case ${HOST} in |
|
8 sunbroy* | atbroy* | macbroy*) |
|
9 DEST=/home/html/isabelle/html-data |
|
10 ;; |
|
11 *.cl.cam.ac.uk) |
|
12 USER=paulson |
|
13 DEST=/anfs/www/html/research/hvg/Isabelle |
|
14 ;; |
|
15 *) |
|
16 echo "Unknown destination directory for ${HOST}" |
|
17 exit 2 |
|
18 ;; |
|
19 esac |
|
20 |
|
21 exec $(dirname $0)/isasync $DEST |