diff options
| author | Gaëtan Gilbert | 2020-02-20 13:58:50 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-20 13:58:50 +0100 |
| commit | aee284e64c97dce0112e36a7f225d14391533f11 (patch) | |
| tree | 23093222cfb6170d51ce2e6fd0756fbebc3e7b64 /Makefile.dev | |
| parent | eaad3ea920fadb5cb710e5e0f110631dc119ea29 (diff) | |
| parent | c65ef8d5714572c4fd21ed4cda3a26c3738d8c35 (diff) | |
Merge PR #11630: [make] Fix makefile variable after plugin .v files move
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
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) |