+ rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \
+ $(PROGRAMS) \
+ $(PROGRAMS_OPT) \
+ $(PROGRAMS_STATIC) \
+ $(PROGRAMS_UPX) \
+ $(NULL)
+
+tests: matitac matitadep matitaclean coq.moo
+ @-(cd library && make -k clean all)
+ @-(cd tests && make -k clean all)
+ @-(cd tests/bad_tests && make -k clean all)
+ @-(cd contribs/LAMBDA-TYPES && make -k clean all)
+ @-(cd contribs/PREDICATIVE-TOPOLOGY && make -k clean all)
+tests.opt: matitac.opt matitadep.opt matitaclean.opt
+ @-(cd library && make -k clean.opt opt)
+ @-(cd tests && make -k clean.opt opt)
+ @-(cd tests/bad_tests && make -k clean.opt opt)
+ @-(cd contribs/LAMBDA-TYPES && make -k clean.opt opt)
+ @-(cd contribs/PREDICATIVE-TOPOLOGY && make -k clean.opt opt)
+cleantests: matitaclean
+ @(cd library && make clean)
+ @(cd tests && make clean)
+ @(cd tests/bad_tests && make clean)
+ @(cd contribs/LAMBDA-TYPES && make clean)
+ @(cd contribs/PREDICATIVE-TOPOLOGY && make clean)
+cleantests.opt: matitaclean.opt
+ @(cd library && make clean.opt)
+ @(cd tests && make clean.opt)
+ @(cd tests/bad_tests && make clean)
+ @(cd contribs/LAMBDA-TYPES && make clean.opt)
+ @(cd contribs/PREDICATIVE-TOPOLOGY && make clean.opt)
+.PHONY: tests tests.opt cleantests cleantests.opt
+
+# {{{ Distribution stuff
+
+STATIC_LINK = dist/static_link/static_link
+# for matita
+STATIC_LIBS = \
+ t1 t1x \
+ gtkmathview_gmetadom mathview mathview_backend_gtk mathview_frontend_gmetadom \
+ gtksourceview-1.0 \
+ gdome gmetadom_gdome_cpp_smart \
+ stdc++ \
+ mysqlclient \
+ expat \
+ $(NULL)
+STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++
+# for matitac & co
+STATIC_CLIBS = \
+ gdome \
+ mysqlclient \
+ $(NULL)
+STATIC_EXTRA_CLIBS =
+PROGRAMS_STATIC = $(patsubst %,%.static,$(PROGRAMS_OPT))
+PROGRAMS_UPX = $(patsubst %,%.upx,$(PROGRAMS_STATIC))
+
+ifeq ($(HAVE_OCAMLOPT),yes)
+static: $(STATIC_LINK) $(PROGRAMS_STATIC) coq.moo.opt
+else
+upx:
+ @echo "Native code compilation is disabled"
+static:
+ @echo "Native code compilation is disabled"
+endif
+
+$(STATIC_LINK):
+ $(MAKE) -C dist/ $(STATIC_LINK)
+
+matita.opt.static: $(STATIC_LINK) $(LIBX_DEPS) $(CMXS) matita.ml
+ $(STATIC_LINK) $(STATIC_LIBS) -- \
+ $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \
+ $(STATIC_EXTRA_LIBS)
+ strip $@
+dump_moo.opt.static: $(STATIC_LINK) buildTimeConf.cmx dump_moo.ml
+ $(STATIC_LINK) $(STATIC_CLIBS) -- \
+ $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ \
+ $(STATIC_EXTRA_CLIBS)
+ strip $@
+matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
+ $(STATIC_LINK) $(STATIC_CLIBS) -- \
+ $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
+ $(STATIC_EXTRA_CLIBS)
+ strip $@
+# matitadep.opt.static: $(STATIC_LINK) matitadep.ml $(DEPLIB_DEPS) $(DEPCMXS)
+# $(STATIC_LINK) $(STATIC_CLIBS) -- \
+# $(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(DEPCMXS) $< \
+# $(STATIC_EXTRA_CLIBS)
+# strip $@
+matitadep.opt.static: matitac.opt.static
+ @test -f $@ || ln -s $< $@
+# matitaclean.opt.static: $(STATIC_LINK) matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS)
+# $(STATIC_LINK) $(STATIC_CLIBS) -- \
+# $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $< \
+# $(STATIC_EXTRA_CLIBS)
+# strip $@
+matitaclean.opt.static: matitac.opt.static
+ @test -f $@ || ln -s $< $@
+# matitamake.opt.static: $(STATIC_LINK) matitamake.ml $(MAKECMXS)
+# $(STATIC_LINK) $(STATIC_CLIBS) -- \
+# $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(MAKECMXS) $< \
+# $(STATIC_EXTRA_CLIBS)
+# strip $@
+matitamake.opt.static: matitac.opt.static
+ @test -f $@ || ln -s $< $@
+cicbrowser.opt.static: matita.opt.static
+ @test -f $@ || ln -s $< $@
+cicbrowser.opt.static.upx: matita.opt.static.upx
+ @test -f $@ || ln -s $< $@
+
+.PHONY: distclean