Admin/Release/mirror-website
changeset 68750 7087748996af
parent 54674 dae47f997268
equal deleted inserted replaced
68749:714faa6ddd10 68750:7087748996af
     3 # mirrors the Isabelle website
     3 # mirrors the Isabelle website
     4 
     4 
     5 HOST=$(hostname)
     5 HOST=$(hostname)
     6 
     6 
     7 case ${HOST} in
     7 case ${HOST} in
     8   sunbroy* | atbroy* | macbroy* | lxbroy*)
     8   sunbroy* | atbroy* | macbroy* | lxbroy* | lxcisa*)
     9     DEST=/home/html/isabelle/html-data
     9     DEST=/home/html/isabelle/html-data
    10     ;;
    10     ;;
    11   *.cl.cam.ac.uk)
    11   *.cl.cam.ac.uk)
    12     USER=paulson
    12     USER=paulson
    13     DEST=/anfs/bigdisc/lp15/Isabelle
    13     DEST=/anfs/bigdisc/lp15/Isabelle