Change to lowercase path names as directed by local pagemasters
authorpaulson
Mon, 11 May 2009 15:05:17 +0100
changeset 31086 3e69a25b90a2
parent 31085 e270f45ac0ec
child 31093 ee45b1c733c1
child 31094 7d6edb28bdbc
Change to lowercase path names as directed by local pagemasters
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}"