From 05538113ccb6d6f05eb0e5ddee6f1640d0c96764 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 13 Jun 2006 12:03:51 +0000 Subject: [PATCH] - distributed matitaGeneratedGui.ml (needed) - when distributed 'world' is the default target --- Makefile | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 836137656..dfd4b5834 100644 --- a/Makefile +++ b/Makefile @@ -5,13 +5,15 @@ include Makefile.defs SUBDIRS = components matita ifeq ($(DISTRIBUTED),yes) +# 'world' is the default target when distributed, otherwise 'all' is +world: depend $(foreach d,$(SUBDIRS),rec@world@$(d)) all: depend $(foreach d,$(SUBDIRS),rec@all@$(d)) opt: depend $(foreach d,$(SUBDIRS),rec@opt@$(d)) else all: $(foreach d,$(SUBDIRS),rec@all@$(d)) opt: $(foreach d,$(SUBDIRS),rec@opt@$(d)) -endif world: depend $(foreach d,$(SUBDIRS),rec@world@$(d)) +endif depend: depend-stamp depend-stamp: ifeq ($(HAVE_OCAMLOPT),yes) @@ -60,6 +62,9 @@ EXTRA_DIST = \ Makefile \ Makefile.defs.in \ $(NULL) +EXTRA_DIST_matita = \ + matita/matitaGeneratedGui.ml \ + $(NULL) distcheck: dist dist_extract dist_test @@ -83,11 +88,13 @@ dist_export: dist/configure (cd $(DISTDIR) && rm -f $(CLEAN_ON_DIST)) cp $< $(DISTDIR)/configure cp -r $(EXTRA_DIST) $(DISTDIR) + cp -r $(EXTRA_DIST_matita) $(DISTDIR)/matita # distribute HTML version of the manual mkdir -p $(DISTDIR)/docs/manual/ $(MAKE) -C matita/help/C/ install DESTDIR=$(CURDIR)/$(DISTDIR)/docs/manual/ dist_mktarball: tar czf $(DISTDIR).tar.gz $(DISTDIR) + tar cjf $(DISTDIR).tar.bz2 $(DISTDIR) rm -rf $(DISTDIR) dist_extract: -- 2.39.2