From 24951d885fbadb8f2fa96ea44a6d3b2a397eab00 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 1 Jun 2018 10:40:04 +0200 Subject: 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. --- Makefile | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 5f042969..e983db8d 100644 --- a/Makefile +++ b/Makefile @@ -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 -- cgit