-
Notifications
You must be signed in to change notification settings - Fork 184
docs: add a version switch. #1642
New issue
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
Conversation
Yes please. |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #1642 +/- ##
=======================================
Coverage 91.28% 91.28%
=======================================
Files 44 44
Lines 11471 11471
Branches 2236 2236
=======================================
Hits 10471 10471
Misses 837 837
Partials 163 163 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
|
The smoke tests can be ignored (amaranth-soc is having issues due to too-new Python). The check-links test might need an exemption for medium.com. |
6c9e064 to
a94c2e3
Compare
a94c2e3 to
0765235
Compare
Done. I am deeply unhappy with the way it turned out, however; any suggestions as to how the code could be improved are appreciated. |
This patch makes the theme include a JavaScript file that replaces the static version HTML with a
<select>element. The list of versions is fetched from<content root>/../versions.jsonand is expected to adhere to the following format:[ { "name": "1.2.3", "root_url": "/docs/amaranth/v1.2.3/" }, { "name": "1.2.2", "root_url": "/docs/amaranth/v1.2.2/" } ]This file is expected to be updated manually similarly to how updates are done for https://amaranth-lang.org/index.html. However, an automation could be built at a maintainer's request: for example, this file could be assembled anew when pushing from this repo's GitHub Actions workflow to https://github.com/amaranth-lang/amaranth-lang.github.io.
The appearance of the version switch matches that of the Read the Docs theme's version switch.
Once this PR is merged, a follow-up PR should be created for https://github.com/amaranth-lang/amaranth-lang.github.io that adds this JavaScript file to all past versions of the documentation, together with the initial version of the
versions.jsonfile.