From 044cfbc299691320c7f8214be905099f2ee944f6 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 30 Oct 2024 16:49:37 +0100 Subject: [PATCH] Simplify `make documentation` No need to filter-out `doc/coq2html`, it's not part of `$^`. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 93d6a58be..2e52ab7f9 100644 --- a/Makefile +++ b/Makefile @@ -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)