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