- matex: we separate axioms (propositions) and assumptions (other)

[helm.git] / matita / components / binaries / matex / Makefile

diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile
index 42e1360e2b598846187f6641c4c3ea1e1761ee86..b3cc515d2ef748a01192eedb789efdb38fad7816 100644 (file)
--- a/matita/components/binaries/matex/Makefile
+++ b/matita/components/binaries/matex/Makefile
@@ -5,12 +5,22 @@ REQUIRES = helm-ng_library
 
 include ../Makefile.common
 
-REGISTRY = $(RT_BASE_DIR)/matita.conf.xml
+PROBE    = ../probe/probe.native
+REGISTRY = $(RT_BASE_DIR)/matita.conf.xml \
+           test/legacy_1.conf.xml test/ground_1.conf.xml test/basic_1.conf.xml
+OBJS     = Make.objs
+SRCS     = Make.srcs
 
-OBJ = cic:/matita/lambdadelta/basic_1/pr0/pr0/pr0_confluence.con
+DEVEL = ../../../matita/contribs/lambdadelta/basic_1/
 
-test:
-       @echo MaTeX $(OBJ)
-       $(H)./matex.native -O test $(REGISTRY) $(OBJ)
+test: test/$(SRCS)
+
+test/$(OBJS): $(REGISTRY)
+       @echo probe: $(DEVEL)
+       $(H)$(PROBE) $(REGISTRY) -g $(DEVEL) -os > $@
+
+test/$(SRCS): test/$(OBJS) $(REGISTRY) ./matex.native
+       @echo MaTeX: processing $<
+       $(H)./matex.native -O test -l $(SRCS) -a -g -p $(REGISTRY) `cat $<`
 
 .PHONY: test