7e07ef0202
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. |
||
---|---|---|
debian |