Commit 57d808c9 authored by Carlos Garnacho's avatar Carlos Garnacho

build: Toggle developer docs off by default

They are irrelevant to most people and on most situations. Toggling docs
off might save a few cycles globally.
parent d6f408ff
Pipeline #60445 passed with stage
in 1 minute and 54 seconds