Admin/mirror-website
changeset 27594 86db6468145d
parent 25463 8b9c4582795a
child 31086 3e69a25b90a2
equal deleted inserted replaced
27593:602dd4b219c0 27594:86db6468145d
     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