Solution: keep the new --without-docs option, but also keep the old
--without-documentation with an added deprecation warning.
We can then remove it in the next major release, to leave enough time
for users and maintainers to change it without disruptions.