diff --git a/Makefile b/Makefile index c7cadb6f68cc48941bd6b9d2795529dd64258907..451a944a1720671097bc4bcfc757e3751ce2d6a1 100644 --- a/Makefile +++ b/Makefile @@ -17,7 +17,7 @@ NATIVE := true # If defined, the dependencies will be updated automatically. -CHECKDEP := +CHECKDEP := 1 # If defined, it indicates the number of cores # that make should use (e.g. -j2 for two cores). @@ -107,12 +107,11 @@ clean: .PHONY: depend -depend: - $(OCAMLDEP) $(SOURCESMLI) $(SOURCESML) > .depend +depend: .depend ifdef CHECKDEP .depend: $(SOURCESMLI) $(SOURCESML) - $(OCAMLDEP) $(SOURCESMLI) $(SOURCESML) > .depend + $(OCAMLDEP) $(SOURCESMLI) $(SOURCESML) > $@ endif -include .depend +-include .depend