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>
Unfortunately, it doesn't seem like there's a way to have sphinx copy
this without moving the files, becasue html_extra_path doesn't copy the
directory itself when given a directory, only files inside and
subdirectories.
Reviewed-by: Eric Engestrom <eric@engestrom.ch>
Part-of: <https://gitlab.freedesktop.org/mesa/mesa/-/merge_requests/4630>
