# HG changeset patch
# User haftmann
# Date 1242054511 -7200
# Node ID ee45b1c733c16b08c779d89afbcdad2ccdf808c1
# Parent  3e69a25b90a238452f9838725378fa68f95fc825# Parent  27a6558e64b62aef9feffcb77f38b410ee4fabf2
merged

diff -r 27a6558e64b6 -r ee45b1c733c1 Admin/mirror-website
--- 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}"