This directory contains the website: http://math-comp.github.io/math-comp/ What is committed in here goes straight online.
By running make in htmldoc one updates the html files generated by coqdoc and the library graph.
Some html files are actually generated from eponymous org files
(extension .org
). They are generated using emacs: open the file
blah.org
with emacs, press C-c C-e h h
to generate the
corresponding blah.html
.