diff --git a/Makefile b/Makefile index 9f8f99e9b5e3a794996712a698fed3660a7053c8..5bc8f472c95400efff461782caabc19914cf9445 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 \