Gary Verhaegen fd185ed22e publish prerelease documentation (#4976) ... This PR changes the documentation release process to publish the documentation for releases tagged "prerelease" on GitHub, while discarding them when deciding on the latest version (the one that shows on `/` on the docs site) and omitting them from the `versions.json` file (meaning they do not appear on the dropdown). This PR also makes a bit of cleanup/bug fixing: - The change in `nix` toolset name (#4724) needs to be protected by a version check, as we checkout older versions of the repo during docs build. - The data types BlogSubmit and BlogId seem to have survived the "dead code detection" in #4956. - The documentation build step had not been updated to pass down the correct version string (#4513). CHANGELOG_BEGIN CHANGELOG_END		2020-03-12 18:54:47 +00:00
..
src	publish prerelease documentation (#4976)	2020-03-12 18:54:47 +00:00
BUILD.bazel	docs cron: follow github pagination links (#4115)	2020-01-20 18:47:47 +01:00
monthly.yaml	report-std-change: handle GitHub errors (#4814)	2020-03-05 10:06:58 +01:00
run.sh	update copyright notices to 2020 (#3939)	2020-01-02 21:21:13 +01:00