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

@@ -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