aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dev
diff options
context:
space:
mode:
authorWilliam Lawvere2017-07-01 22:10:46 -0700
committerWilliam Lawvere2017-07-01 22:10:46 -0700
commit80649ebaba75838bfd28ae78822cd2c078da4b23 (patch)
treeac29ab5edd3921dbee1c2256737347fd1542dc67 /Makefile.dev
parentc2942e642ee6f83cc997f9a2510cdb7446a65cb4 (diff)
parent35e0f327405fb659c7ec5f9f7d26ea284aa45810 (diff)
Merge remote-tracking branch 'upstream/trunk' into trunk
Diffstat (limited to 'Makefile.dev')
-rw-r--r--Makefile.dev2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.dev b/Makefile.dev
index 0105df972a..b0299bd160 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -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)