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-main
author wenzelm
Wed, 09 Feb 2000 14:03:29 +0100
changeset 8222 55fed562d8ed
child 8225 fc5db20d7f6f
permissions -rwxr-xr-x
mirror main page;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8222
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset 
     1
 
#!/bin/bash
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset 
     2
 
#
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset 
     3
 
# $Id$
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset 
     4
 
#
55fed562d8ed mirror main page;
wenzelm
parents:
diff changeset 
     5
 












55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




     6


case $(hostname) in













55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




     7


  sunbroy30)













55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




     8


    DEST=/home/html/isabelle/html-data













55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




     9


    ;;













55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




    10


  foobar)













55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




    11


    DEST=/foo/bar













55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




    12


    ;;













55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




    13


  *)













55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




    14


    echo "Unknown destination directory!"













55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




    15


    exit 2













55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




    16


    ;;













55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




    17


esac













55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




    18














55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




    19


rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \













55fed562d8ed
mirror main page;



wenzelm


parents: 

diff
changeset




    20


  sunbroy1.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/www/. $DEST/.















isabelle