aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/dune
AgeCommit message (Collapse)Author
2019-02-18Add diff rule for README.rst to dune refman-html aliasGaƫtan Gilbert
We change regen_readme such that when given an argument it outputs there instead of overwriting the readme. Prompted by me noticing I forgot to regen in #9553.
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.