Admin/linktest
author wenzelm
Fri, 13 Mar 2009 19:58:26 +0100
changeset 30510 4120fc59dd85
parent 17750 a0745bc36660
child 36859 51af1657263b
permissions -rwxr-xr-x
unified type Proof.method and pervasive METHOD combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17673
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
     1
#!/usr/bin/env bash
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
     2
#
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
     3
# $Id$
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
     4
#
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
     5
# leightweight link checker for the isabelle website
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
     6
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
     7
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
     8
PRG=`basename "$0"`
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
     9
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    10
usage()
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    11
{
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    12
  echo
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    13
  echo "Usage: $PRG URL"
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    14
  echo
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    15
  exit 1
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    16
}
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    17
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    18
fail()
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    19
{
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    20
  echo "$1" >&2
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    21
  exit 2
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    22
}
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    23
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    24
url="$1"
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    25
if [ -z "$url" ]
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    26
then
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    27
  usage;
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    28
fi
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    29
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    30
type -p ggrep > /dev/zero && GREP=ggrep || GREP=grep
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    31
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    32
mkdir -p /tmp/isa_linktest
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    33
dir=$(pwd)
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    34
cd /tmp/isa_linktest
17750
a0745bc36660 improved linktest
haftmann
parents: 17674
diff changeset
    35
exec wget --non-verbose --cookies=off --recursive --reject='GraphBrowser.class' --convert-links --page-requisites \
17673
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    36
   --delete-after \
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    37
  "$url" \
17750
a0745bc36660 improved linktest
haftmann
parents: 17674
diff changeset
    38
  2>&1 | tee /tmp/isa_linktest.report | "$GREP" -i -B1 "ERROR"
17673
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    39
cd "$dir"
b61966d74ff1 added simple linktester for isabelle website
haftmann
parents:
diff changeset
    40
rm -rf /tmp/isa_linktest