changeset 8224 | 97e26127fb6b |
child 8322 | 6ba8356baa34 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/mirror-dist Wed Feb 09 14:35:23 2000 +0100 @@ -0,0 +1,17 @@ +#!/bin/bash +# +# $Id$ +# + +case $(hostname) in + foobar) + DEST=/foo/bar/dist + ;; + *) + echo "Unknown destination directory!" + exit 2 + ;; +esac + +rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \ + sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/.