summaryrefslogtreecommitdiff
path: root/dev-ml/num/files
diff options
context:
space:
mode:
authorV3n3RiX <venerix@koprulu.sector>2022-01-16 20:27:28 +0000
committerV3n3RiX <venerix@koprulu.sector>2022-01-16 20:27:28 +0000
commit2fd57282f0262ca084e05b0f2c63fbada395d02b (patch)
tree4e0f23cea9ce9fd972e70ebc5214bf36fed465cc /dev-ml/num/files
parentc3bc61051d7f12b4c682efa7a5460bbc8815649e (diff)
gentoo resync : 16.01.2021
Diffstat (limited to 'dev-ml/num/files')
-rw-r--r--dev-ml/num/files/num-1.4-ocamlopt.patch15
1 files changed, 15 insertions, 0 deletions
diff --git a/dev-ml/num/files/num-1.4-ocamlopt.patch b/dev-ml/num/files/num-1.4-ocamlopt.patch
new file mode 100644
index 000000000000..90699b99474c
--- /dev/null
+++ b/dev-ml/num/files/num-1.4-ocamlopt.patch
@@ -0,0 +1,15 @@
+--- a/src/Makefile 2022-01-12 19:58:54.655901110 +0100
++++ b/src/Makefile 2022-01-12 19:59:25.446339664 +0100
+@@ -33,11 +33,10 @@
+
+ all:: libnums.$(A) nums.cma
+
++ifeq "$(NATDYNLINK)" "true"
+ ifneq "$(ARCH)" "none"
+ all:: nums.cmxa
+ endif
+-
+-ifeq "$(NATDYNLINK)" "true"
+ all:: nums.cmxs
+ endif
+