From c22e64ac3cb2a0e60a3289c03c4f7f0eff6a7d46 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 26 Sep 2005 16:02:35 +0000 Subject: [PATCH] matitatop.opt should not be generated --- helm/matita/Makefile.in | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 301eb2efc..76183c0e5 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -62,10 +62,11 @@ CCMOS = \ $(NULL) CLEANCMOS = $(CCMOS) MAKECMOS = $(CCMOS) -PROGRAMS = matita matitac matitatop cicbrowser matitadep matitaclean matitamake -PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS)) +PROGRAMS_BYTE = matita matitac cicbrowser matitadep matitaclean matitamake +PROGRAMS = $(PROGRAMS_BYTE) matitatop dump_moo +PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) -all: matita.conf.xml $(PROGRAMS) dump_moo +all: matita.conf.xml $(PROGRAMS) matita.conf.xml: matita.conf.xml.sample @if diff matita.conf.xml.sample matita.conf.xml 1>/dev/null 2>/dev/null; then\ -- 2.39.2