Allows to avoid verbose logging. The option is now used in user-doc/extract to simplify the generation of code-specific notes (cherry picked from commit 7152d46f) Conflicts: patches/patch.sh
