DocBook: Avoid building man pages repeatedly and inconsistently

DocBook: Avoid building man pages repeatedly and inconsistently

Some kernel-doc sections are included in multiple DocBook files.  This
means the mandocs target will generate the same manual page multiple
times with different metadata (author name/address and manual title,
taken from the including DocBook file).  If it's invoked in a parallel
build, the output is nondeterminstic.

For each section that is duplicated, mark the less specific manual's
inclusion as 'extra' and exclude it during conversion to manual pages.
Use xmlif for this, as that is bundled with xmlto which we already
use.

I would have preferred to use more conventional markup for this, but
each of the following approaches failed:

1. Wrap the extra inclusions with a new element and add a template to
   the stylesheet to include/exclude them.  Unfortunately DocBook XSL
   doesn't seem to support foreign elements at an intermediate level
   in the document tree.
2. Use DocBook profiling.  This works but requires passing an absolute
   path to the profile stylesheet to xmlto, so it's not portable.
3. Use SGML marked sections.  docbook2x can handle these but xmlto
   chokes on them.

Reported-by: Jérémy Bobbio <lunar@debian.org>
Signed-off-by: Ben Hutchings <ben@decadent.org.uk>
Signed-off-by: Jonathan Corbet <corbet@lwn.net>