]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/Makefile
New target librarytest (to apply testlibrary.opt to index.txt). The output
[helm.git] / helm / gTopLevel / Makefile
index 8a41c7dc25f8bac87bf85161578b841f3c7ec1e0..7ea740bc6430e4a4017d9e09720f12791c5060d0 100644 (file)
@@ -97,6 +97,8 @@ test: regtest
        ./regtest $(INTESTS) 2> /dev/null
 envtest: regtest
        ./regtest -dump $(INTESTS) 2> /dev/null
+librarytest: testlibrary.opt
+       ./testlibrary.opt - <index.txt 2>/dev/null >LOG &
 
 ifneq ($(MAKECMDGOALS), depend)
    include .depend