diff options
Diffstat (limited to 'Makefile.dev')
| -rw-r--r-- | Makefile.dev | 3 |
1 files changed, 1 insertions, 2 deletions
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) |