removed useless grepping -v

[helm.git] / helm / software / matita / template_makefile.in

diff --git a/helm/software/matita/template_makefile.in b/helm/software/matita/template_makefile.in
index 57f1301d57e9e265dc1aeaa68f3ca23ac930d063..d24c75b0ff36858fa85c02248929546a73af01bd 100644 (file)
--- a/helm/software/matita/template_makefile.in
+++ b/helm/software/matita/template_makefile.in
@@ -19,7 +19,7 @@ clean:
        rm -f $(TODO)
 
 %.moo:
-       ($(MATITAC) $(MATITA_FLAGS) -q -I @ROOT@ $< | (grep -v "^make" || true))
+       $(MATITAC) $(MATITA_FLAGS) -q -I @ROOT@ $<
 
 @DEPFILE@ : $(SRC)
        $(MATITADEP) $(MATITA_FLAGS) -I '@ROOT@' $^ 1> @DEPFILE@