Fully disable building and installing any documentation when the nodoc
build-profile is used.
Among other things this will help reducing build times when doing
development builds, especially on IO-limited build workers.
We don't want to include "-4.9" in them twice. Add a "source_basename"
template variable that excludes any version suffix in the source package
name.
(cherry picked from commit f3c51efdd6e9d0ce32ee5a0f998fdcda930a715c)
For master, nothing is immediately broken without this. Also we have
no longer build a linux-manual package. Change the changelog text
accordingly.
It has finally been removed after all docs were converted to ReST format.
As there is no longer a way to build manpages, remove the linux-manual
package.