From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 5 Feb 2004 18:15:45 +0000 (+0000)
Subject: New target librarytest (to apply testlibrary.opt to index.txt). The output
X-Git-Tag: V_0_2_3~27
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a6d9bfd36f9ae6bce95d886eb41ea561dc0cb755;p=helm.git

New target librarytest (to apply testlibrary.opt to index.txt). The output
is in LOG.
---

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index 8a41c7dc2..7ea740bc6 100644
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -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