diff options
| author | Théo Zimmermann | 2020-03-10 16:39:50 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-10 16:39:50 +0100 |
| commit | d1e0b777052bb94eff8226a57c40f0558308b10e (patch) | |
| tree | f91252e8b6588e395a7dbbf84bae0814195c1ab9 /lib/system.ml | |
| parent | 3a5469b2097c55ecf952ead470caf03b6112cd9e (diff) | |
Remove parallel building of Sphinx documentation.
Since version 1.0.0 of the sphinxcontrib-bibtex extension, parallel
building of the Sphinx documentation emits a warning (and thus makes
our warning-free build fail).
This change was already done in Makefile.doc as part of #11732.
Diffstat (limited to 'lib/system.ml')
0 files changed, 0 insertions, 0 deletions