| Age | Commit message (Collapse) | Author |
|---|
|
This is actually supported by Sphinx directly.
|
|
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
|
|
Dependencies specified through an alias do not trigger a rebuild when
they are modified. This is likely a Dune bug, but we still need to
fix this on our side as this is inconvenient.
|
|
|
|
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.
|
|
|
|
Move existing entries.
|
|
Instead, if the coqlib is special, we set it explicitly in the command
line, as Dune does.
This is a continuation of #9523.
In Sphinx, we stop using -boot, and pass `-coqlib` through the
environment instead.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
The way to override this default is not exactly the same as in the legacy Makefile
but it has been documented as well.
|
|
This is a reduced version of #8503 as to provide a way to build the
reference manual with Dune.
Dune 1.6 supports (experimentally) directories as targets, thus we
introduce a rule that will call `sphinx` to build the manual.
This only provides build, however generation of `.install` rules is
not done, it will be hopefully addressed in #8503.
Note that we set `expire: 1 month` for all the artifacts we build with
Dune. IMHO this makes most sense as not to abuse Gitlab's hosting,
however of course we could consider a different deployment strategy if
wanted.
|
