Andrew Morgan 4c807ca305 Port new changes to mdbook default theme to our copy ...

The custom theme is still needed for the version picker. Technically we
could add this HTML in the version-picker.js, but there's no guarantee
that the HTML IDs etc. wouldn't change out from under us.

We also no longer need the next/prev hiding plugin, as the original
point of it was to prevent those UI elements from interfering with our
custom TOC.

2026-01-07 15:04:06 +00:00

..

index.hbs

Port new changes to mdbook default theme to our copy

2026-01-07 15:04:06 +00:00