]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/Makefile
delift no longer apply the substitution when a Meta is found.
[helm.git] / helm / gTopLevel / Makefile
index 0f3318ab29340e6163adddc1d748aa7f4efcd128..ec10354a78bb2217da342dc32cd8d5b2245f5769 100644 (file)
@@ -81,16 +81,16 @@ uninstall:
 .PHONY: install uninstall clean test
 
 INTESTS := $(wildcard tests/*.cic)
-OUTTESTS := $(patsubst %, %.test, $INTESTS)
+OUTTESTS := $(patsubst %, %.test, $(INTESTS))
 gentest: $(OUTTESTS)
 cleantest:
        rm -f $(OUTTESTS)
 tests/%.cic.test: tests/%.cic regtest
        time ./regtest -gen $<
 test:
-       time ./regtest $(INTESTS)
+       ./regtest $(INTESTS) 2> /dev/null
 envtest:
-       time ./regtest -dump $(INTESTS)
+       ./regtest -dump $(INTESTS) 2> /dev/null
 
 ifneq ($(MAKECMDGOALS), depend)
    include .depend