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