Admin/mirror-website
changeset 31086 3e69a25b90a2
parent 27594 86db6468145d
child 36859 51af1657263b
equal deleted inserted replaced
31085:e270f45ac0ec 31086:3e69a25b90a2
    10   sunbroy* | atbroy* | macbroy*)
    10   sunbroy* | atbroy* | macbroy*)
    11     DEST=/home/html/isabelle/html-data
    11     DEST=/home/html/isabelle/html-data
    12     ;;
    12     ;;
    13   *.cl.cam.ac.uk)
    13   *.cl.cam.ac.uk)
    14     USER=paulson
    14     USER=paulson
    15     DEST=/anfs/www/html/Research/HVG/Isabelle
    15     DEST=/anfs/www/html/research/hvg/Isabelle
    16     ;;
    16     ;;
    17   *)
    17   *)
    18     echo "Unknown destination directory for ${HOST}"
    18     echo "Unknown destination directory for ${HOST}"
    19     exit 2
    19     exit 2
    20     ;;
    20     ;;