make MATITAC="../scripts/do_tests.sh ../matitac /dev/null"

can now be used to benchmark the output

diff --git a/helm/matita/library/Makefile b/helm/matita/library/Makefile
index 24417790f316abc37e555606571555665c14b4bb..10944f4704899fb3bd716c9c6ab9c0f31d3ca960 100644 (file)
--- a/helm/matita/library/Makefile
+++ b/helm/matita/library/Makefile
@@ -6,6 +6,8 @@ SRC=\
        nat.ma \
         Z.ma
 
+MATITAC=../matitac
+
 DEPEND_NAME=.depend
 LINKS=.matita matita.lang matita.conf.xml
 
@@ -19,7 +21,7 @@ depend: $(DEPEND_NAME)
 
 %.moo:%.ma depend $(LINKS)
        [ ! -e $@ ] || ../matitaclean $< 
-       ../matitac $< || ../matitaclean $<
+       $(MATITAC) $< || ../matitaclean $<
 
 $(DEPEND_NAME): $(SRC) $(LINKS)
        ../matitadep $(SRC) > $@