This PR redirects all generated documentation pages to their new location.
Basically, as there were only a few html files, these now only include a <meta http-equiv="redirect"> tag to make the browser redirect to the new location. There is also a tiny bit of javascript that adds the hash to the redirection URL if available.
This PR redirects all generated documentation pages to their new location.
Basically, as there were only a few html files, these now only include a
<meta http-equiv="redirect">tag to make the browser redirect to the new location. There is also a tiny bit of javascript that adds the hash to the redirection URL if available.