diff options
| -rw-r--r-- | otherlibs/dynlink/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/otherlibs/dynlink/Makefile b/otherlibs/dynlink/Makefile index fad42995d..597131e2b 100644 --- a/otherlibs/dynlink/Makefile +++ b/otherlibs/dynlink/Makefile @@ -37,7 +37,7 @@ extract_crc: dynlink.cma extract_crc.cmo $(CAMLC) $(COMPFLAGS) -o extract_crc dynlink.cma extract_crc.cmo install: - cp dynlink.cmi dynlink.cma extract_crc $(LIBDIR) + cp dynlink.cmi dynlink.cma dynlink.mli extract_crc $(LIBDIR) installopt: |