Uniform headers in HTML pages

The version number is now also automatically updated in the page headers
for 'make html'.  Also, fix most links in the file format pages.
If we in the future move into some proper HTML publishing system (e.g.,
based on Markdown), it should probably take care of this and also
cross-links between these pages and the generated pages, so not much
effort has been put to make the approach or the headers/footers
particularly elegant.

Related to #685 and #1242.

Change-Id: I083d1f9714ddf68dfc2977799378299a43a05b73