Admin/linktest
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 17750 a0745bc36660
child 36859 51af1657263b
permissions -rwxr-xr-x
setup: theory -> theory;
haftmann@17673
     1
#!/usr/bin/env bash
haftmann@17673
     2
#
haftmann@17673
     3
# $Id$
haftmann@17673
     4
#
haftmann@17673
     5
# leightweight link checker for the isabelle website
haftmann@17673
     6
haftmann@17673
     7
haftmann@17673
     8
PRG=`basename "$0"`
haftmann@17673
     9
haftmann@17673
    10
usage()
haftmann@17673
    11
{
haftmann@17673
    12
  echo
haftmann@17673
    13
  echo "Usage: $PRG URL"
haftmann@17673
    14
  echo
haftmann@17673
    15
  exit 1
haftmann@17673
    16
}
haftmann@17673
    17
haftmann@17673
    18
fail()
haftmann@17673
    19
{
haftmann@17673
    20
  echo "$1" >&2
haftmann@17673
    21
  exit 2
haftmann@17673
    22
}
haftmann@17673
    23
haftmann@17673
    24
url="$1"
haftmann@17673
    25
if [ -z "$url" ]
haftmann@17673
    26
then
haftmann@17673
    27
  usage;
haftmann@17673
    28
fi
haftmann@17673
    29
haftmann@17673
    30
type -p ggrep > /dev/zero && GREP=ggrep || GREP=grep
haftmann@17673
    31
haftmann@17673
    32
mkdir -p /tmp/isa_linktest
haftmann@17673
    33
dir=$(pwd)
haftmann@17673
    34
cd /tmp/isa_linktest
haftmann@17750
    35
exec wget --non-verbose --cookies=off --recursive --reject='GraphBrowser.class' --convert-links --page-requisites \
haftmann@17673
    36
   --delete-after \
haftmann@17673
    37
  "$url" \
haftmann@17750
    38
  2>&1 | tee /tmp/isa_linktest.report | "$GREP" -i -B1 "ERROR"
haftmann@17673
    39
cd "$dir"
haftmann@17673
    40
rm -rf /tmp/isa_linktest