equal
deleted
inserted
replaced
5 # mirrors the Isabelle website |
5 # mirrors the Isabelle website |
6 |
6 |
7 HOST=$(hostname) |
7 HOST=$(hostname) |
8 |
8 |
9 case ${HOST} in |
9 case ${HOST} in |
10 sunbroy2) |
10 sunbroy* | atbroy* | macbroy*) |
11 DEST=/home/html/isabelle/html-data |
|
12 ;; |
|
13 atbroy*) |
|
14 DEST=/home/html/isabelle/html-data |
11 DEST=/home/html/isabelle/html-data |
15 ;; |
12 ;; |
16 *.cl.cam.ac.uk) |
13 *.cl.cam.ac.uk) |
17 USER=paulson |
14 USER=paulson |
18 DEST=/anfs/www/html/Research/HVG/Isabelle |
15 DEST=/anfs/www/html/Research/HVG/Isabelle |