Admin/mirror-main
changeset 8225 fc5db20d7f6f
parent 8222 55fed562d8ed
child 8321 dc13f558856d
equal deleted inserted replaced
8224:97e26127fb6b 8225:fc5db20d7f6f
     5 
     5 
     6 case $(hostname) in
     6 case $(hostname) in
     7   sunbroy30)
     7   sunbroy30)
     8     DEST=/home/html/isabelle/html-data
     8     DEST=/home/html/isabelle/html-data
     9     ;;
     9     ;;
    10   foobar)
    10   *.cl.cam.ac.uk)
    11     DEST=/foo/bar
    11     USER=paulson
       
    12     DEST=/anfs/www/html/Research/HVG/Isabelle
    12     ;;
    13     ;;
    13   *)
    14   *)
    14     echo "Unknown destination directory!"
    15     echo "Unknown destination directory for $(hostname)!"
    15     exit 2
    16     exit 2
    16     ;;
    17     ;;
    17 esac
    18 esac
    18 
    19 
    19 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
    20 rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
    20   sunbroy1.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/www/. $DEST/.
    21   $USER@sunbroy1.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/www/. $DEST/.