merged
authorhaftmann
Mon, 11 May 2009 17:08:31 +0200
changeset 31093 ee45b1c733c1
parent 31086 3e69a25b90a2 (diff)
parent 31092 27a6558e64b6 (current diff)
child 31097 a09767ab684d
child 31103 9820999467a7
child 31108 0ce5f53fc65d
merged
--- a/Admin/mirror-website	Mon May 11 11:53:21 2009 +0200
+++ b/Admin/mirror-website	Mon May 11 17:08:31 2009 +0200
@@ -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}"