A patch from Helmut Grohne to add an option to disable building the docs
Review Request #945 — Created Sept. 26, 2021 and submitted — Latest diff uploaded
A patch from Helmut Grohne to add an option to disable building the docs
Built with the option on and off.