Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Admin/mirror-dist
author paulson
Wed, 16 Feb 2000 10:50:57 +0100
changeset 8248 d7e85fd09291
parent 8224 97e26127fb6b
child 8322 6ba8356baa34
permissions -rwxr-xr-x
a smaller point size reduces the number of overfull figures
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/.















isabelle