diff options
| author | Emilio Jesus Gallego Arias | 2020-09-10 21:58:31 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-09-17 15:27:48 +0200 |
| commit | 2eb778033fe37fa26adaf41d48fc630ef66c9d1d (patch) | |
| tree | e28252dc8d989e9e5c43b87e2e37044372a35661 /tools | |
| parent | 14f0e5059e7f49cabbcd1571d7f053db7d7d3f35 (diff) | |
[build] Don't link `num` anymore in Coq
After #8743 we don't depend on `num` anymore in the codebase; thus we
drop the dependency.
This could create problems for plugins relying on this implicit
linking.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 2 |
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 |