diff options
| author | Emilio Jesus Gallego Arias | 2020-04-28 17:41:18 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-28 20:48:18 +0200 |
| commit | 03ce3fc9ef0bb85d43bb5351b5d109bd0d6743c1 (patch) | |
| tree | 006154f8629d1b12a002c280e2b9a83aae3d05e1 /dev | |
| parent | 16559843925f3489b61920ff398680f10f1f00cc (diff) | |
[doc] [sphinx] Run in silent mode by default
The convention in the dune build is to be silent except for warnings
and errors, so they don't go unnoticed.
We could have this controlled by a variable if needed (likely would
require some support from Dune?)
Solves part of #12194
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions