| 1 |
#! /bin/sh |
| 2 |
|
| 3 |
generate_links() |
| 4 |
{ |
| 5 |
#local index_file name file lineno |
| 6 |
|
| 7 |
index_file="$1" |
| 8 |
|
| 9 |
command='sed ' |
| 10 |
{ |
| 11 |
while read file lineno name; do |
| 12 |
command="$command -e "\''s,\['"$name"'\],<A NAME="'"$name"'">,g'\' |
| 13 |
command="$command -e "\''s,«'"$name"'»,<A HREF="'"$file"\#"$name"'">'"$name"'</A>,g'\' |
| 14 |
done |
| 15 |
} < "$index_file" |
| 16 |
|
| 17 |
eval "$command" |
| 18 |
} |
| 19 |
|
| 20 |
generate_headers() |
| 21 |
{ |
| 22 |
# local index_file name this_file |
| 23 |
|
| 24 |
index_file_generate_headers="$1" |
| 25 |
this_file_generate_headers=`echo $2 | sed 's,.*/,,' | sed 's,\..*$,,'` |
| 26 |
|
| 27 |
name_generate_headers=`grep "^$this_file_generate_headers" "$index_file_generate_headers" | head -1 | sed s,'^[^ ]* [^ ]* ,,'` |
| 28 |
sed 's,<HTML>,<HTML>\ |
| 29 |
<HEAD>\ |
| 30 |
<TITLE>'"$name_generate_headers"'</TITLE>\ |
| 31 |
</HEAD>,' |
| 32 |
} |
| 33 |
|
| 34 |
|
| 35 |
cat "$2" | generate_links "$1" | generate_headers "$1" "$2" |