diff options
| author | lmamane | 2007-07-16 09:43:19 +0000 |
|---|---|---|
| committer | lmamane | 2007-07-16 09:43:19 +0000 |
| commit | e45135c43acd75a604da1b3eb6c90c161d064400 (patch) | |
| tree | f34f6a0efa842b7ec4a5dd3d04cdd3b56bac650e | |
| parent | e23b0a503781a9c1c59ac9f98edae2b3a3c442f7 (diff) | |
Oups... empty .ml4.d files produced
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10009 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index aa2da49a26..3887dfdec7 100644 --- a/Makefile.build +++ b/Makefile.build @@ -812,8 +812,7 @@ endif # NOT to generate object code. %.ml4.d: %.ml4 $(SHOW)'CAMLP4DEPS $<' - $(HIDE)echo > "$@" -# $(HIDE)( echo -n '$*.cmo $*.cmx $*.ml4.ml.d: ' && $(CAMLP4DEPS) "$<" ) > "$@" + $(HIDE)( echo -n '$*.cmo $*.cmx $*.ml4.ml.d: ' && $(CAMLP4DEPS) "$<" ) > "$@" %.ml4.ml.d: %.ml4 | $(GENFILES) $(ML4FILES:.ml4=.ml) %.ml4.d #Critical section: |