$title
+ +$date
EOF } -html_page_creation_notice() { +html_end_of_content() { cat <This page is automatically generated.
Please contact @@ -57,9 +91,9 @@ realmakepage() { cat <
for distribution(s): $descr
-You might also want to check out UDD instead of this page.
+You might also want to check out UDD instead of this page.
@@ -91,7 +125,7 @@ tags:
EOF
./bugreport -H -l $filter
- html_page_creation_notice
+ html_end_of_content
html_closing_tags
}
@@ -100,11 +134,11 @@ makemainpage() {
local title="$1" # Title of page
local date_time="$2" # Date
- header "$title" "$date_time"
+ html_header "$title" "$date_time"
cat <
EOF
./bugreport -Hs
@@ -112,7 +146,7 @@ EOF
cat < Other graphs:
+
@@ -156,7 +190,7 @@ EOF
EOF
- html_page_creation_notice
+ html_end_of_content
cat <