]> 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 abe03e42deea4548ab18076141e04d2f86a318cc..ec10354a78bb2217da342dc32cd8d5b2245f5769 100644 (file)
@@ -80,12 +80,17 @@ uninstall:
 
 .PHONY: install uninstall clean test
 
-TESTS := $(patsubst %, %.test, $(wildcard tests/*.cic))
-gentest: $(TESTS)
-tests/%.cic.test: tests/%.cic
-       ./regtest -gen $<
+INTESTS := $(wildcard tests/*.cic)
+OUTTESTS := $(patsubst %, %.test, $(INTESTS))
+gentest: $(OUTTESTS)
+cleantest:
+       rm -f $(OUTTESTS)
+tests/%.cic.test: tests/%.cic regtest
+       time ./regtest -gen $<
 test:
-       ./regtest $(TESTS)
+       ./regtest $(INTESTS) 2> /dev/null
+envtest:
+       ./regtest -dump $(INTESTS) 2> /dev/null
 
 ifneq ($(MAKECMDGOALS), depend)
    include .depend