Admin/mirror-dist
changeset 8224 97e26127fb6b
child 8322 6ba8356baa34
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/mirror-dist	Wed Feb 09 14:35:23 2000 +0100
     1.3 @@ -0,0 +1,17 @@
     1.4 +#!/bin/bash
     1.5 +#
     1.6 +# $Id$
     1.7 +#
     1.8 +
     1.9 +case $(hostname) in
    1.10 +  foobar)
    1.11 +    DEST=/foo/bar/dist
    1.12 +    ;;
    1.13 +  *)
    1.14 +    echo "Unknown destination directory!"
    1.15 +    exit 2
    1.16 +    ;;
    1.17 +esac
    1.18 +
    1.19 +rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
    1.20 +  sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/.