Skip to content

Commit

Permalink
Simplify make documentation
Browse files Browse the repository at this point in the history
No need to filter-out `doc/coq2html`, it's not part of `$^`.
  • Loading branch information
xavierleroy committed Oct 30, 2024
1 parent aee355d commit 044cfbc
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -266,7 +266,7 @@ documentation: $(FILES)
rm -f doc/html/*.html
coq2html -d doc/html/ -base compcert -short-names \
$(patsubst %, %/*.glob, $(DIRS)) \
$(filter-out doc/coq2html cparser/Parser.v, $^)
$(filter-out cparser/Parser.v, $^)

tools/ndfun: tools/ndfun.ml
ifeq ($(OCAML_NATIVE_COMP),true)
Expand Down

0 comments on commit 044cfbc

Please sign in to comment.