Admin/mirror-main
changeset 14229 bf89038cf551
parent 13567 7f5bf04095bd
child 16278 dda44b201c4d
equal deleted inserted replaced
14228:a1956417c6c1 14229:bf89038cf551
    10 #
    10 #
    11 
    11 
    12 HOST=$(hostname)
    12 HOST=$(hostname)
    13 
    13 
    14 case ${HOST} in
    14 case ${HOST} in
    15   sunbroy51)
    15   atbroy1)
    16     DEST=/home/html/isabelle/html-data
    16     DEST=/home/html/isabelle/html-data
    17     ;;
    17     ;;
    18   *.cl.cam.ac.uk)
    18   *.cl.cam.ac.uk)
    19     USER=paulson
    19     USER=paulson
    20     DEST=/anfs/www/html/Research/HVG/Isabelle
    20     DEST=/anfs/www/html/Research/HVG/Isabelle