Magnus Hagander e6f529dd4e Store the git hash of developer docs loaded ...

This will require some further updates on the loading side of things
before it's fully valid, but for now track and show a link to the git
hash used to build developer docs *if* one is specified.

We only track it for devel (because releases have release numbers) and
we only show it in the cases where we would already show the loading
time.

2022-06-20 20:32:05 +02:00

..

.gitignore

…

docload.py

Store the git hash of developer docs loaded

2022-06-20 20:32:05 +02:00