diff --git a/otherlibs/num/Makefile b/otherlibs/num/Makefile
index 4264d9bab3..431e3341ca 100644
--- a/otherlibs/num/Makefile
+++ b/otherlibs/num/Makefile
@@ -36,7 +36,7 @@ bignum/libbignum.a:
 install:
 	cp libnums.a $(LIBDIR)/libnums.a
 	cd $(LIBDIR); $(RANLIB) libnums.a
-	cp nums.cma $(CMIFILES) $(LIBDIR)
+	cp nums.cma $(CAMLINTF) $(LIBDIR)
 
 installopt:
 	cp nums.cmxa nums.a $(LIBDIR)