Skip to content

Commit

Permalink
add coqdoc parameter improvements from RegLang
Browse files Browse the repository at this point in the history
  • Loading branch information
palmskog committed Mar 1, 2020
1 parent 4f4cc78 commit 5677b59
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion Makefile.coq.local
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,8 @@ HTMLFILES = resources/header.html resources/footer.html
COQDOCDIR = docs/coqdoc

COQDOCHTMLFLAGS = --toc --toc-depth 2 --index indexpage --html \
--interpolate --no-lib-name --parse-comments \
--external 'https://math-comp.github.io/htmldoc/' mathcomp \
--interpolate --no-lib-name --parse-comments \
--with-header resources/header.html --with-footer resources/footer.html

coqdoc: $(GLOBFILES) $(VFILES) $(CSSFILES) $(JSFILES) $(HTMLFILES)
Expand Down

0 comments on commit 5677b59

Please sign in to comment.