Admin/mirror-website

recovered tooltip Entity content (odd effect of layer change!? cf. 806878ae2219);

+
−#!/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