- distributed matitaGeneratedGui.ml (needed)

- when distributed 'world' is the default target

diff --git a/helm/software/Makefile b/helm/software/Makefile
index 83613765669d2421ff69b0586fb56293b2901b4f..dfd4b58341d6fea4a9a0d99ce5463685f2fb2c5f 100644 (file)
--- a/helm/software/Makefile
+++ b/helm/software/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: