diff options
| author | Enrico Tassi | 2017-07-03 16:44:21 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2017-08-02 16:47:54 +0200 |
| commit | 8995d0857277019b54c24672439d3e19b2fcb5af (patch) | |
| tree | 8f35256f93be58008cb1effce4d4f1954b962250 /kernel/nativelambda.ml | |
| parent | 1f46ff6db53c2ca471d9ea067d0824755b2f34da (diff) | |
Makefile.doc: implement serve-refman-8080 target
We make it so that, by default, the HTML reference manual looks
like the one published online (same .css) and we provide a target
to serve it locally (requires python).
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions