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;
wenzelm@8224
     1
#!/bin/bash
wenzelm@8224
     2
#
wenzelm@8224
     3
# $Id$
wenzelm@8224
     4
#
wenzelm@8224
     5
wenzelm@8224
     6
case $(hostname) in
wenzelm@8224
     7
  foobar)
wenzelm@8224
     8
    DEST=/foo/bar/dist
wenzelm@8224
     9
    ;;
wenzelm@8224
    10
  *)
wenzelm@8224
    11
    echo "Unknown destination directory!"
wenzelm@8224
    12
    exit 2
wenzelm@8224
    13
    ;;
wenzelm@8224
    14
esac
wenzelm@8224
    15
wenzelm@8224
    16
rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
wenzelm@8224
    17
  sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/.