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 -e 's,<TITLE>.*</TITLE>,<TITLE>'"$name_generate_headers"'</TITLE>,' \ |
29 |
-e 's,<title>.*</title>,<title>'"$name_generate_headers"'</title>,' |
30 |
} |
31 |
|
32 |
|
33 |
cat "$2" | generate_links "$1" | generate_headers "$1" "$2" |