aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
Commit message (Expand)AuthorAge
* gitlab: build sphinx doc in separate jobGravatar Gaëtan Gilbert2018-06-08
* [doc] Fix an incorrect use of $PWD in Makefile.docGravatar Clément Pit-Claudel2018-05-22
* Sphinx: a "QUICK=1" option to bypass recompilation of the library.Gravatar Hugo Herbelin2018-05-12
* Clean-up in Makefile.doc and include Sphinx in doc-html target.Gravatar Théo Zimmermann2018-05-10
* Remove tutorials.Gravatar Théo Zimmermann2018-05-10
* [doc] Remove unused dependencies.Gravatar Emilio Jesus Gallego Arias2018-04-28
* Remove LaTeX refman, now that migration to Sphinx is completeGravatar Maxime Dénès2018-04-16
* [Sphinx] Build with warnings as errorsGravatar Maxime Dénès2018-04-14
* [Sphinx] Move chapter 9 to new infrastructure.Gravatar Théo Zimmermann2018-04-14
* [Sphinx] Move chapter 1 to new infrastructureGravatar Maxime Dénès2018-04-13
* [Sphinx] Move chapter 29 to new infrastructureGravatar Maxime Dénès2018-04-11
* [Sphinx] Move chapter 6 to new infrastructureGravatar Maxime Dénès2018-04-10
* [Sphinx] Move chapter 15 to new infrastructureGravatar Maxime Dénès2018-04-10
* [Sphinx] Move chapter 7 to new infrastructureGravatar Maxime Dénès2018-04-09
* [Sphinx] Move chapter 30 to new infrastructureGravatar Maxime Dénès2018-04-05
* [Sphinx] Move chapter 28 to new infrastructureGravatar Maxime Dénès2018-04-04
* [Sphinx] Move chapter 27 to new infrastructureGravatar Maxime Dénès2018-03-30
* [Sphinx] Move chapter 25 to new infrastructureGravatar Maxime Dénès2018-03-30
* [Sphinx] Move chapter 26 to new infrastructureGravatar Maxime Dénès2018-03-29
* [Sphinx] Move chapter 24 to new infrastructureGravatar Maxime Dénès2018-03-29
* [Sphinx] Move chapter 23 to new infrastructureGravatar Maxime Dénès2018-03-29
* [Sphinx] Move chapter 18 to new infrastructureGravatar Maxime Dénès2018-03-29
* Move Classes.tex to type-classes.rstGravatar Matthieu Sozeau2018-03-26
* Merge branch 'master' into sphinx-doc-chapter-22Gravatar Guillaume Melquiond2018-03-22
|\
| * Merge branch 'master' into sphinx-doc-chapter-21Gravatar Guillaume Melquiond2018-03-22
| |\
| | * Merge branch 'master' into sphinx-doc-chapter-19Gravatar Guillaume Melquiond2018-03-22
| | |\
* | | | [Sphinx] Move chapter 22 to new infrastructureGravatar Maxime Dénès2018-03-22
| * | | [Sphinx] Move chapter 21 to new infrastructureGravatar Maxime Dénès2018-03-22
|/ / /
| * / [Sphinx] Move chapter 19 to new infrastructureGravatar Maxime Dénès2018-03-22
|/ /
| * [Sphinx] Move chapter 17 to new infrastructureGravatar Maxime Dénès2018-03-22
|/
* [Sphinx] Add chapter 11Gravatar Maxime Dénès2018-03-16
* [Sphinx] Move chapter 3 to new infrastructureGravatar Maxime Dénès2018-03-15
* [Sphinx] Move chapter 16 to new infrastructureGravatar Maxime Dénès2018-03-15
* [Sphinx] Move chapter 14 to new infrastructureGravatar Maxime Dénès2018-03-15
* [Sphinx] Move chapter 13 to new infrastructureGravatar Maxime Dénès2018-03-15
* [Sphinx] Move chapter 12 to new infrastructureGravatar Maxime Dénès2018-03-15
* [Sphinx] Move chapter 10 to new infrastructureGravatar Maxime Dénès2018-03-15
* [Sphinx] Move chapter 8 to new infrastructureGravatar Maxime Dénès2018-03-15
* [Sphinx] Move chapter 5 to new infrastructureGravatar Maxime Dénès2018-03-15
* [Sphinx] Move chapter 4 to new infrastructureGravatar Maxime Dénès2018-03-15
* [Sphinx] Add chapter 2Gravatar Maxime Dénès2018-03-15
* [Sphinx] Move chapter 2 to new infrastructureGravatar Maxime Dénès2018-03-15
* [Sphinx] Move credits to new infrastructureGravatar Maxime Dénès2018-03-15
* [Sphinx] Move introduction to new infrastructureGravatar Maxime Dénès2018-03-13
* Integration of a sphinx-based documentation generator.Gravatar Maxime Dénès2018-03-09
* Remove NOPLUGINDOCS optionGravatar mrmr19932018-03-05
* Build docs for plugins by default, add NOPLUGINDOCS flag to disableGravatar mrmr19932018-03-05
* Tidy up ml-doc outut, give it a separate output directoryGravatar mrmr19932018-03-05
* Use computed deps to generate ml-doc and use implicit mli-doc depsGravatar mrmr19932018-03-05
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\