equal
deleted
inserted
replaced
4 # |
4 # |
5 |
5 |
6 HOST=$(hostname) |
6 HOST=$(hostname) |
7 |
7 |
8 case ${HOST} in |
8 case ${HOST} in |
|
9 sunbroy79) |
|
10 #test |
|
11 DEST=/tmp/isabelle-dist |
|
12 mkdir -p $DEST |
|
13 ;; |
9 *.cl.cam.ac.uk) |
14 *.cl.cam.ac.uk) |
10 USER=paulson |
15 USER=paulson |
11 DEST=/anfs/www/html/Research/HVG/Isabelle/dist |
16 DEST=/anfs/www/html/Research/HVG/Isabelle/dist |
12 ;; |
|
13 sunbroy79) |
|
14 DEST=/tmp/isabelle-dist |
|
15 ;; |
17 ;; |
16 *) |
18 *) |
17 echo "Unknown destination directory for ${HOST}" |
19 echo "Unknown destination directory for ${HOST}" |
18 exit 2 |
20 exit 2 |
19 ;; |
21 ;; |