Admin/mirror-dist
changeset 8346 562090b1f128
parent 8323 64b67ed25a59
child 8347 8927067ef107
     1.1 --- a/Admin/mirror-dist	Mon Mar 06 12:04:39 2000 +0100
     1.2 +++ b/Admin/mirror-dist	Mon Mar 06 15:24:07 2000 +0100
     1.3 @@ -12,7 +12,6 @@
     1.4      mkdir -p $DEST
     1.5      ;;
     1.6    *.cl.cam.ac.uk)
     1.7 -    USER=paulson
     1.8      DEST=/anfs/www/html/Research/HVG/Isabelle/dist
     1.9      ;;
    1.10    *)
    1.11 @@ -22,4 +21,4 @@
    1.12  esac
    1.13  
    1.14  rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
    1.15 -  $USER@sunbroy30.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/. $DEST/.
    1.16 +  rsync://sunbroy30.informatik.tu-muenchen.de:8730/isabelle-dist/. $DEST/.