e037761a2f
I'm not sure why I picked html_extra_path instead, as it's meant for slightly less directly related files than what html_static_path is for. So let's switch. It shouldn't make much of a real-world difference, but should make it a bit easier to understand what this is about. Reviewed-by: Corentin Noël <corentin.noel@collabora.com> Part-of: <https://gitlab.freedesktop.org/mesa/mesa/-/merge_requests/25585>