# HG changeset patch # User paulson # Date 1242050717 -3600 # Node ID 3e69a25b90a238452f9838725378fa68f95fc825 # Parent e270f45ac0ec0875519f6c7fab67d60994a6719c Change to lowercase path names as directed by local pagemasters diff -r e270f45ac0ec -r 3e69a25b90a2 Admin/mirror-website --- a/Admin/mirror-website Sun May 10 14:22:04 2009 +0200 +++ b/Admin/mirror-website Mon May 11 15:05:17 2009 +0100 @@ -12,7 +12,7 @@ ;; *.cl.cam.ac.uk) USER=paulson - DEST=/anfs/www/html/Research/HVG/Isabelle + DEST=/anfs/www/html/research/hvg/Isabelle ;; *) echo "Unknown destination directory for ${HOST}"