mirror of
https://github.com/gentoo-mirror/gentoo.git
synced 2026-08-05 12:38:09 -07:00
15 lines
441 B
Diff
15 lines
441 B
Diff
--- a/src/Makefile 2025-08-24 20:37:54.276261621 +0200
|
|
+++ b/src/Makefile 2025-08-24 20:34:04.708721094 +0200
|
|
@@ -156,9 +156,9 @@
|
|
|
|
install: num-top-install
|
|
$(INSTALL_DIR) $(DESTDIR)$(STDLIBDIR)
|
|
- cp META.num META
|
|
+ mv META.num META
|
|
$(OCAMLFIND) install num META
|
|
- rm -f META
|
|
+ mv META META.num
|
|
$(INSTALL_DATA) $(TOINSTALL) $(DESTDIR)$(STDLIBDIR)
|
|
ifeq "$(NATDYNLINK)" "true"
|
|
$(INSTALL_DLL) $(TOINSTALL_CMXS) $(DESTDIR)$(STDLIBDIR)
|