a further step toward releasable Makefile

diff --git a/helm/matita/Makefile b/helm/matita/Makefile
index 40a4b2014b97dbfb09ace795ac569d362fb3c1ea..415d4a1a557488ac594162a4c21b34d67ad59a6a 100644 (file)
--- a/helm/matita/Makefile
+++ b/helm/matita/Makefile
@@ -190,8 +190,15 @@ cleantests.opt: $(foreach d,$(TEST_DIRS),$(d)-cleantests-opt)
 
 # {{{ Distribution stuff
 
+ifeq ($(HAVE_OCAMLOPT),yes)
+BEST=opt
+else
+BEST=all
+endif
+
 stdlib:
-       $(MAKE) MATITA_FLAGS="-system" -C library/
+       MATITA_RT_BASE_DIR=`pwd` \
+               $(MAKE) MATITA_FLAGS="-system" -C library/ $(BEST)
 
 DEST = @RT_BASE_DIR@
 INSTALL_STUFF =                        \
@@ -213,6 +220,7 @@ endif
 
 install:
        install -d $(DEST)
+       cp -a .matita/
        cp -a $(INSTALL_STUFF) $(DEST)
 uninstall: