#!/bin/csh -f

# Change anchors and links in files all included in current document
# to internal links and targets.  Does the processing on standard
# input with $1 indicating the file name.  Assumes anchor or link
# (including link text) is on a single line.

sed 's+<A NAME="\([^"]*\)">+\\hypertarget{'"$1"':\1}{}+\
     s+<A HREF="\([^#]*\)#\([^"]*\)">\(.*\)</A>+\\hyperlink{\1:\2}{\3}+'