diff options
| author | Emilio Jesus Gallego Arias | 2020-02-19 08:45:14 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-19 08:45:14 -0500 |
| commit | c65ef8d5714572c4fd21ed4cda3a26c3738d8c35 (patch) | |
| tree | 6b5e3ee55c162956b19c30a59b0723417e3a047f /Makefile.dev | |
| parent | 43c3c7d6f62a9bee4772242c27fbafd54770d271 (diff) | |
[make] Fix makefile variable after plugin .v files move
This is a bug due to #11529
Diffstat (limited to 'Makefile.dev')
| -rw-r--r-- | Makefile.dev | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/Makefile.dev b/Makefile.dev index b1e142333a..6e9b5356ab 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -140,17 +140,17 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \ ### 4) plugins ################ -OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO)) -MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO)) -RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO)) -NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO)) -FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO)) -BTAUTOVO:=$(filter plugins/btauto/%, $(PLUGINSVO)) -RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO)) -EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO)) +OMEGAVO:=$(filter theories/omega/%, $(THEORIESVO)) +MICROMEGAVO:=$(filter theories/micromega/%, $(THEORIESVO)) +RINGVO:=$(filter theories/setoid_ring/%, $(THEORIESVO)) +NSATZVO:=$(filter theories/nsatz/%, $(THEORIESVO)) +FUNINDVO:=$(filter theories/funind/%, $(THEORIESVO)) +BTAUTOVO:=$(filter theories/btauto/%, $(THEORIESVO)) +RTAUTOVO:=$(filter theories/rtauto/%, $(THEORIESVO)) +EXTRACTIONVO:=$(filter theories/extraction/%, $(THEORIESVO)) CCVO:= -DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO)) -LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO)) +DERIVEVO:=$(filter theories/derive/%, $(THEORIESVO)) +LTACVO:=$(filter theories/ltac/%, $(THEORIESVO)) omega: $(OMEGAVO) $(OMEGACMO) micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) |