From 2b90ded10b3d5124999c8a91eb2b9ccea78e3c1a Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Tue, 29 Oct 2024 16:54:39 +0100
Subject: [PATCH] Use GNU make's wildcard expansion instead of the shell's,
 because the shell will leave a export/*.glob item in there if there are no
 export/*.glob files. The Makefile only works with gmake anyway. It would be
 possible to use option nullglob in bash, but many systems now use dash.

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index bf173f4b1..001611f4f 100644
--- a/Makefile
+++ b/Makefile
@@ -261,7 +261,7 @@ documentation: $(FILES)
 	mkdir -p doc/html
 	rm -f doc/html/*.html
 	coq2html -d doc/html/ -base compcert -short-names \
-	  $(patsubst %, %/*.glob, $(DIRS)) \
+	  $(wildcard $(patsubst %, %/*.glob, $(DIRS))) \
           $(filter-out doc/coq2html cparser/Parser.v, $^)
 
 tools/ndfun: tools/ndfun.ml