From a1f10626bed1db14ce116e9201ed05dadfc366b4 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 11 Sep 2018 14:32:22 +0200
Subject: Remove romega

---
 Makefile.dev | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'Makefile.dev')

diff --git a/Makefile.dev b/Makefile.dev
index 2a7e61126a..82b81908ac 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -169,7 +169,6 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \
 ################
 
 OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO))
-ROMEGAVO:=$(filter plugins/romega/%, $(PLUGINSVO))
 MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO))
 RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO))
 NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO))
@@ -181,7 +180,7 @@ CCVO:=
 DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO))
 LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO))
 
-omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
+omega: $(OMEGAVO) $(OMEGACMO)
 micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
 setoid_ring: $(RINGVO) $(RINGCMO)
 nsatz: $(NSATZVO) $(NSATZCMO)
-- 
cgit v1.2.3