From e26af75ba820444fc1500fe21cb3d4c40e28a71c Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 16 Jul 2021 16:07:19 +0200
Subject: [PATCH] [Makefile] add missing wildcard
---
Makefile | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/Makefile b/Makefile
index 9f8f99e9b5e..5bc8f472c95 100644
--- a/Makefile
+++ b/Makefile
@@ -243,7 +243,7 @@ DISTRIB_FILES:=\
$(THEME_ICONS_FLAT) \
man/frama-c.1 doc/README \
doc/code/docgen.ml \
- doc/code/*.css doc/code/intro_plugin.txt \
+ $(wildcard doc/code/*.css) doc/code/intro_plugin.txt \
doc/code/intro_plugin_D_and_S.txt \
doc/code/intro_plugin_default.txt \
doc/code/intro_kernel_plugin.txt \
--
GitLab