author | wenzelm |
Mon, 14 Jul 2008 23:28:26 +0200 | |
changeset 27594 | 86db6468145d |
parent 27593 | 602dd4b219c0 |
child 27595 | 3ac9e3cd1fa3 |
--- a/Admin/mirror-website Mon Jul 14 23:11:20 2008 +0200 +++ b/Admin/mirror-website Mon Jul 14 23:28:26 2008 +0200 @@ -7,10 +7,7 @@ HOST=$(hostname) case ${HOST} in - sunbroy2) - DEST=/home/html/isabelle/html-data - ;; - atbroy*) + sunbroy* | atbroy* | macbroy*) DEST=/home/html/isabelle/html-data ;; *.cl.cam.ac.uk)