aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dev
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.dev')
-rw-r--r--Makefile.dev4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.dev b/Makefile.dev
index fde92ec949..b0299bd160 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -120,7 +120,7 @@ highparsing: parsing/highparsing.cma
stm: stm/stm.cma
toplevel: toplevel/toplevel.cma
-.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping
+.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping API
.PHONY: engine highparsing stm toplevel
######################
@@ -186,7 +186,7 @@ omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
setoid_ring: $(RINGVO) $(RINGCMO)
nsatz: $(NSATZVO) $(NSATZCMO)
-extraction: $(EXTRACTIONCMO)
+extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO)
fourier: $(FOURIERVO) $(FOURIERCMO)
funind: $(FUNINDCMO) $(FUNINDVO)
cc: $(CCVO) $(CCCMO)