diff options
Diffstat (limited to 'tools/Makefile.shared')
| -rw-r--r-- | tools/Makefile.shared | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/Makefile.shared b/tools/Makefile.shared index b50cb0adde..6b33a5b047 100644 --- a/tools/Makefile.shared +++ b/tools/Makefile.shared @@ -89,7 +89,7 @@ install:: cp profiling.cmi profiling.cmo $(INSTALL_LIBDIR) installopt:: - cp profiling.cmx profiling.o $(INSTALL_LIBDIR) + cp profiling.cmx profiling.$(O) $(INSTALL_LIBDIR) clean:: rm -f ocamlprof ocamlcp ocamloptp |