On Fri, 8 Nov 2019 at 11:39, Stefan Hajnoczi <stefa...@gmail.com> wrote: > > On Fri, Nov 8, 2019 at 11:52 AM Peter Maydell <peter.mayd...@linaro.org> > wrote: > > So the reason I went for the odd "run sphinx multiple times" > > approach was because we don't want to ship 'devel' to users, > > and as far as I could tell there was no way to have a > > single-invocation build of the docs not include it in > > eg the index/search (which would then be broken when > > we don't install devel/ as part of 'make install'). > > Does this patchset result in a set of installed docs > > that don't have dangling references ? > > You are right: > * The hidden documents are included in the navigation bar (different > from the table of contents). > * The search index (which install-doc omits!) includes content from > the hidden documents. > > I have asked on #sphinx-doc. Let's see if there is a solution.
FWIW, this is the thread where I asked on the sphinx-users list about the best way to handle "multiple manuals but we only ship a subset": https://www.mail-archive.com/sphinx-users@googlegroups.com/msg03224.html > It might be possible to hack docs/config.py to exclude devel/ when run > from make install-sphinxdocs > (https://www.sphinx-doc.org/en/master/usage/configuration.html#confval-exclude_patterns). > This requires building the docs again at install time but the > advantage is we get a single searchable set of documentation. Yeah, if you're willing to build the docs twice (once for local and once for installed) that also works. I'd prefer not to do build work at 'make install' time, though -- if we want to do this we should build them twice at 'make' time and install just the right one. thanks -- PMM