mirror of
https://github.com/AdaCore/gpr.git
synced 2026-02-12 12:58:39 -08:00
We do all the work inside Sphinx, instead of requiring a change in the Makefile: we generate html titles ids through Sphinx we call pagefind though sphinx instead As a bonus, we introduce a small extension dedicated to pagefind. Comes from the work of Boris Yakobowski <yakobowski@adacore.com>