]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/utilities/Makefile
Several instances of the same bug fixed at once: when processing a Fix,
[helm.git] / helm / software / components / binaries / utilities / Makefile
index 314136db57dabda1d015fd7df4f030898d4c8e53..1874a238543eb464f05813e53a522c2366ec644f 100644 (file)
@@ -23,7 +23,19 @@ depend:
        $(H)ocamldep extractor.ml extractor_manager.ml > .depend
 depend.opt: 
        $(H)echo "  OCAMLDEP -native"
-       $(H)ocamldep -native extractor.ml extractor_manager.ml > .depend
+       $(H)ocamldep -native extractor.ml extractor_manager.ml > .depend.opt
+       
+ifeq ($(MAKECMDGOALS),)
+  include .depend   
+endif
 
+ifeq ($(MAKECMDGOALS), all)
+  include .depend   
+endif
+
+ifeq ($(MAKECMDGOALS), opt)
+  include .depend.opt   
+endif
+       
 include ../../../Makefile.defs