Admin/mirror-main
changeset 9286 4ccadbdbbd24
parent 8321 dc13f558856d
child 12721 226fc0e2e7e3
equal deleted inserted replaced
9285:21bfc8c14c3d 9286:4ccadbdbbd24
     4 #
     4 #
     5 
     5 
     6 HOST=$(hostname)
     6 HOST=$(hostname)
     7 
     7 
     8 case ${HOST} in
     8 case ${HOST} in
     9   sunbroy30)
     9   sunbroy51)
    10     DEST=/home/html/isabelle/html-data
    10     DEST=/home/html/isabelle/html-data
    11     ;;
    11     ;;
    12   *.cl.cam.ac.uk)
    12   *.cl.cam.ac.uk)
    13     USER=paulson
    13     USER=paulson
    14     DEST=/anfs/www/html/Research/HVG/Isabelle
    14     DEST=/anfs/www/html/Research/HVG/Isabelle