--- a/Admin/mirror-main Wed Feb 09 14:35:23 2000 +0100
+++ b/Admin/mirror-main Thu Feb 10 11:03:54 2000 +0100
@@ -7,14 +7,15 @@
sunbroy30)
DEST=/home/html/isabelle/html-data
;;
- foobar)
- DEST=/foo/bar
+ *.cl.cam.ac.uk)
+ USER=paulson
+ DEST=/anfs/www/html/Research/HVG/Isabelle
;;
*)
- echo "Unknown destination directory!"
+ echo "Unknown destination directory for $(hostname)!"
exit 2
;;
esac
rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va \
- sunbroy1.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/www/. $DEST/.
+ $USER@sunbroy1.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/www/. $DEST/.