diff --git a/doc/tools/texi2www/texi2www b/doc/tools/texi2www/texi2www index 91c6cc14db..84dc9924f8 100755 --- a/doc/tools/texi2www/texi2www +++ b/doc/tools/texi2www/texi2www @@ -19,11 +19,15 @@ $usage = <\n"); &printHTML("\n"); + &print_header if $header; &printHTML("\n$this\n"); &printHTML("\n") if $next; &printHTML("\n") if $prev; @@ -906,6 +913,20 @@ sub printHTML } } # printHTML +######################################################################## +sub print_header +{ + unless (open(HEADER,$header)) { + print "WARNING -- couldn't open header file \"$header\" -- $!\n"; + $header = 0; + return; + } + while (
) { + &printHTML($_); + } + close(HEADER); +} + ######################################################################## sub print_footer {