Admin/mirror-website
2009-05-11 paulson 2009-05-11 Change to lowercase path names as directed by local pagemasters
2008-07-14 wenzelm 2008-07-14 cover macbroy as well; tuned;
2007-11-26 haftmann 2007-11-26 simplified website rsync
2005-11-15 wenzelm 2005-11-15 better no -d option;
2005-09-27 haftmann 2005-09-27 website preparation for Isabelle2005