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