Admin/mirror-website

--- a/Admin/mirror-website	Thu Jul 05 13:35:46 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-#!/usr/bin/env bash
-#
-# mirrors the Isabelle website
-
-HOST=$(hostname)
-
-case ${HOST} in
-  sunbroy* | atbroy* | macbroy*)
-    DEST=/home/html/isabelle/html-data
-    ;;
-  *.cl.cam.ac.uk)
-    USER=paulson
-    DEST=/anfs/www/html/research/hvg/Isabelle
-    ;;
-  *)
-    echo "Unknown destination directory for ${HOST}"
-    exit 2
-    ;;
-esac
-
-exec $(dirname $0)/isasync $DEST