dropped obsolete script
authorhaftmann
Wed, 02 Jun 2010 11:36:09 +0200
changeset 37251b79df37bbdc4
parent 37250 e7544b9ce6af
child 37276 87988eeed572
child 37287 9834c21c4ba1
dropped obsolete script
Admin/linktest
     1.1 --- a/Admin/linktest	Wed Jun 02 08:01:45 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,38 +0,0 @@
     1.4 -#!/usr/bin/env bash
     1.5 -#
     1.6 -# leightweight link checker for the isabelle website
     1.7 -
     1.8 -
     1.9 -PRG=`basename "$0"`
    1.10 -
    1.11 -usage()
    1.12 -{
    1.13 -  echo
    1.14 -  echo "Usage: $PRG URL"
    1.15 -  echo
    1.16 -  exit 1
    1.17 -}
    1.18 -
    1.19 -fail()
    1.20 -{
    1.21 -  echo "$1" >&2
    1.22 -  exit 2
    1.23 -}
    1.24 -
    1.25 -url="$1"
    1.26 -if [ -z "$url" ]
    1.27 -then
    1.28 -  usage;
    1.29 -fi
    1.30 -
    1.31 -type -p ggrep > /dev/zero && GREP=ggrep || GREP=grep
    1.32 -
    1.33 -mkdir -p /tmp/isa_linktest
    1.34 -dir=$(pwd)
    1.35 -cd /tmp/isa_linktest
    1.36 -exec wget --non-verbose --cookies=off --recursive --reject='GraphBrowser.class' --convert-links --page-requisites \
    1.37 -   --delete-after \
    1.38 -  "$url" \
    1.39 -  2>&1 | tee /tmp/isa_linktest.report | "$GREP" -i -B1 "ERROR"
    1.40 -cd "$dir"
    1.41 -rm -rf /tmp/isa_linktest