Merge commit '8c201dde'

* commit '8c201dde':
  build: doc: more fine-grained dependencies for generated texi files

This commit is a noop, we have a different system for handling the
documentation.
Merged-by: Clément Bœsch <u@pkh.me>