Admin/mirror-dist
author wenzelm
Wed Feb 09 14:35:23 2000 +0100 (2000-02-09)
changeset 8224 97e26127fb6b
child 8322 6ba8356baa34
permissions -rwxr-xr-x
mirror dist page;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 
     6 case $(hostname) in
     7   foobar)
     8     DEST=/foo/bar/dist
     9     ;;
    10   *)
    11     echo "Unknown destination directory!"
    12     exit 2
    13     ;;
    14 esac
    15 
    16 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
    17   sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/.