Admin/mirror-website
author wenzelm
Wed Mar 19 22:28:17 2008 +0100 (2008-03-19 ago)
changeset 26338 f8ed02f22433
parent 25463 8b9c4582795a
child 27594 86db6468145d
permissions -rwxr-xr-x
auxiliary dynamic_thm(s) for fact lookup;
renamed local dynamic_thm(s) to goal_thm(s);
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 #
     5 # mirrors the Isabelle website
     6 
     7 HOST=$(hostname)
     8 
     9 case ${HOST} in
    10   sunbroy2)
    11     DEST=/home/html/isabelle/html-data
    12     ;;
    13   atbroy*)
    14     DEST=/home/html/isabelle/html-data
    15     ;;
    16   *.cl.cam.ac.uk)
    17     USER=paulson
    18     DEST=/anfs/www/html/Research/HVG/Isabelle
    19     ;;
    20   *)
    21     echo "Unknown destination directory for ${HOST}"
    22     exit 2
    23     ;;
    24 esac
    25 
    26 exec $(dirname $0)/isasync $DEST