From 5a99efb2b5eec9678f453345b9b70160b36ae6cf Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 7 Feb 2006 10:53:01 +0000 Subject: [PATCH] removed useless grepping -v --- matita/template_makefile.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matita/template_makefile.in b/matita/template_makefile.in index 57f1301d5..d24c75b0f 100644 --- a/matita/template_makefile.in +++ b/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@ -- 2.39.2