# HG changeset patch
# User haftmann
# Date 1275471369 -7200
# Node ID b79df37bbdc46d7b390deffe9b029cfc5aa04cba
# Parent  e7544b9ce6afd87019fcc668d4b012c1c660a700
dropped obsolete script

diff -r e7544b9ce6af -r b79df37bbdc4 Admin/linktest
--- a/Admin/linktest	Wed Jun 02 08:01:45 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-#!/usr/bin/env bash
-#
-# leightweight link checker for the isabelle website
-
-
-PRG=`basename "$0"`
-
-usage()
-{
-  echo
-  echo "Usage: $PRG URL"
-  echo
-  exit 1
-}
-
-fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-url="$1"
-if [ -z "$url" ]
-then
-  usage;
-fi
-
-type -p ggrep > /dev/zero && GREP=ggrep || GREP=grep
-
-mkdir -p /tmp/isa_linktest
-dir=$(pwd)
-cd /tmp/isa_linktest
-exec wget --non-verbose --cookies=off --recursive --reject='GraphBrowser.class' --convert-links --page-requisites \
-   --delete-after \
-  "$url" \
-  2>&1 | tee /tmp/isa_linktest.report | "$GREP" -i -B1 "ERROR"
-cd "$dir"
-rm -rf /tmp/isa_linktest