aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-09-30 09:54:35 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-09-30 09:54:35 +0200
commit504018731249475d1ab57a97e7cbd3842b13e984 (patch)
tree74e0d1b6dc9be57ccc5d503ebda032e9f15579a6 /Makefile.build
parenta478947e33bcca34291ec36487876443a694c6bf (diff)
Build the compatibility files.
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build
index 39f60bd59..30b93a0e8 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -524,7 +524,7 @@ hightactics: tactics/hightactics.cma
.PHONY: init theories theories-light
.PHONY: logic arith bool narith zarith qarith lists strings sets
.PHONY: fsets relations wellfounded reals setoids sorting numbers noreal
-.PHONY: msets mmaps
+.PHONY: msets mmaps compat
init: $(INITVO)
@@ -554,6 +554,7 @@ structures: $(STRUCTURESVO)
vectors: $(VECTORSVO)
msets: $(MSETSVO)
mmaps: $(MMAPSVO)
+compat: $(COMPATVO)
noreal: unicode logic arith bool zarith qarith lists sets fsets \
relations wellfounded setoids sorting