# HG changeset patch
# User haftmann
# Date 1242064271 -7200
# Node ID 9820999467a709de1df455292c246781d49dce9b
# Parent  f1e3100e6c499b0d6f20bbb23ab7cc627034e66e# Parent  ee45b1c733c16b08c779d89afbcdad2ccdf808c1
merged

diff -r f1e3100e6c49 -r 9820999467a7 Admin/mirror-website
--- a/Admin/mirror-website	Mon May 11 15:57:30 2009 +0200
+++ b/Admin/mirror-website	Mon May 11 19:51:11 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}"