Admin/mirror-dist
author nipkow
Wed Aug 04 11:25:08 2004 +0200 (2004-08-04)
changeset 15106 e8cef6993701
parent 13567 7f5bf04095bd
permissions -rwxr-xr-x
aded comment
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 #
     5 # Mirrors the Isabelle distribution pages and downloads. 
     6 #
     7 # It does *not* mirror the home page (those directly on 
     8 # http://isabelle.in.tum.de). There is a separate utility 
     9 # (mirror-main) for that.
    10 #
    11 # Usage: mirror-dist
    12 #
    13 
    14 
    15 HOST=$(hostname)
    16 
    17 case ${HOST} in
    18   sunbroy*)
    19     #test
    20     DEST=/tmp/isabelle-dist
    21     mkdir -p $DEST
    22     ;;
    23   *.cl.cam.ac.uk)
    24     DEST=/anfs/www/html/Research/HVG/Isabelle/dist
    25     ;;
    26   *)
    27     echo "Unknown destination directory for ${HOST}"
    28     exit 2
    29     ;;
    30 esac
    31 
    32 exec $(dirname $0)/rsync-isabelle -d $DEST