GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
I think the following would be nice slight improvements to the header:
Calling the PDF file "print" isn't very useful - if someone saves it for offline reading or something, it's an extremely uninformative name. (I'm annoyed by the large number of download sites that give all files some useless name like "download".)
That seem like a separate issue to change the filename, introduce redirects, etc.
We could add a Content-Disposition header with a suggested filename of "HTML Standard.pdf" if the primary concern is downloads. That doesn't seem too hard.
Hmm, we already did that in 9f3a811.
More tweaks to header links