diff --git a/Makefile.generating b/Makefile.generating index 72bb05086dc3d74f22384335468404f96e6f1d1d..1b3a85d837c0fd69ed24b35fbc5f958824ae5eae 100644 --- a/Makefile.generating +++ b/Makefile.generating @@ -177,6 +177,7 @@ endif .PHONY:merlin .merlin merlin: share/Makefile.config Makefile.generating #create Merlin file + $(PRINT_MAKING) $@ echo "FLG -c $(FLAGS) $(FRAMAC_USER_MERLIN_FLAGS)" > .merlin for PKG in $(LIBRARY_NAMES); do echo PKG $$PKG >> .merlin; done for PKG in $(LIBRARY_NAMES_GUI); do echo PKG $$PKG >> .merlin; done