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