Skip to content

Commit

Permalink
Website update
Browse files Browse the repository at this point in the history
'
  • Loading branch information
ianshil committed Feb 29, 2024
1 parent 23bef66 commit b71a78c
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
EXTRA_DIR:= doc-config
COQDOCFLAGS:= \
--toc --toc-depth 2 --html --interpolate \
-d docs \
--index indexpage --no-lib-name --parse-comments \
--with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html
export COQDOCFLAGS
Expand Down

0 comments on commit b71a78c

Please sign in to comment.