doc: add support for an optional navigation bar in texi2html pages
The navigation header for the web pages lives in a different repository. Read it during documentation regeneration to use the same navigation bar on all pages.
Showing
Please
register
or
sign in
to comment