aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-09-17 16:16:39 +0000
committerGitHub2020-09-17 16:16:39 +0000
commit08791151b904e499cdca26cec4b8aa7c9b1eb4c0 (patch)
tree583b907530ea9c77bdec3d1bf11488f7ef5d00c1 /tools
parent14f0e5059e7f49cabbcd1571d7f053db7d7d3f35 (diff)
parent29b8aae282f03fcd7d753d19129e5f74feacc820 (diff)
Merge PR #13007: [build] Don't link `num` anymore in Coq
Reviewed-by: Zimmi48 Reviewed-by: vbgl Ack-by: Zimmi48 Ack-by: vbgl
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 02ababd928..0ebb97d0bf 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -104,7 +104,7 @@ BEFORE ?=
AFTER ?=
# FIXME this should be generated by Coq (modules already linked by Coq)
-CAMLDONTLINK=str,unix,dynlink,threads,num,zarith
+CAMLDONTLINK=str,unix,dynlink,threads,zarith
# OCaml binaries
CAMLC ?= "$(OCAMLFIND)" ocamlc -c