diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-01 10:40:04 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-01 10:40:04 +0200 |
| commit | 24951d885fbadb8f2fa96ea44a6d3b2a397eab00 (patch) | |
| tree | c048b0745667c4a00298c302948ddf7afdc5deba /Makefile | |
| parent | ffc03f2dcb24438d2900743848005c9a058e649c (diff) | |
| download | compcert-24951d885fbadb8f2fa96ea44a6d3b2a397eab00.tar.gz compcert-24951d885fbadb8f2fa96ea44a6d3b2a397eab00.zip | |
Use the standalone coq2html tool to generate the HTML documentation
coq2html is now a standalone project (https://github.com/xavierleroy/coq2html)
packaged as coq-coq2html in OPAM-Coq.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 12 |
1 files changed, 2 insertions, 10 deletions
@@ -177,18 +177,11 @@ FORCE: .PHONY: proof extraction runtime FORCE -documentation: doc/coq2html $(FILES) +documentation: $(FILES) mkdir -p doc/html rm -f doc/html/*.html - doc/coq2html -o 'doc/html/%.html' doc/*.glob \ + coq2html -d doc/html/ -base compcert -short-names doc/*.glob \ $(filter-out doc/coq2html cparser/Parser.v, $^) - cp doc/coq2html.css doc/coq2html.js doc/html/ - -doc/coq2html: doc/coq2html.ml - ocamlopt -w +a-29 -o doc/coq2html str.cmxa doc/coq2html.ml - -doc/coq2html.ml: doc/coq2html.mll - ocamllex -q doc/coq2html.mll tools/ndfun: tools/ndfun.ml ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml @@ -268,7 +261,6 @@ clean: rm -f $(patsubst %, %/*.vo, $(DIRS)) rm -f $(patsubst %, %/.*.aux, $(DIRS)) rm -rf doc/html doc/*.glob - rm -f doc/coq2html.ml doc/coq2html doc/*.cm? doc/*.o rm -f driver/Version.ml rm -f compcert.ini rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr |