aboutsummaryrefslogtreecommitdiff
path: root/doc/dune
AgeCommit message (Collapse)Author
2019-05-05Create categories in changelog.Théo Zimmermann
2019-05-05New infrastructure for the unreleased changelog.Théo Zimmermann
Move existing entries.
2019-02-14[coqlib] Remove `-boot` option for setting the coqlibEmilio Jesus Gallego Arias
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>
2018-12-26[dune] Build refman with fatal warnings by default like in the Makefile build.Théo Zimmermann
The way to override this default is not exactly the same as in the legacy Makefile but it has been documented as well.
2018-12-13[dune] [doc] Support for building the reference manual with Dune.Emilio Jesus Gallego Arias
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.