diff options
| -rw-r--r-- | tools/coq_makefile.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 02bba6cfef..15df485b60 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -448,6 +448,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles) other_targets inc print "MLLIBFILES:="; print_list "\\\n " l; print "\n"; print "\n-include $(MLLIBFILES:.mllib=.mllib.d)\n.SECONDARY: $(MLLIBFILES:.mllib=.mllib.d)\n\n"; print "CMAFILES:=$(MLLIBFILES:.mllib=.cma)\n"; + classify_files_by_root "CMAFILES" l inc; print "CMXAFILES:=$(CMAFILES:.cma=.cmxa)\n"; end; begin match mlifiles with |