diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-24 01:06:46 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-24 01:11:28 +0200 |
| commit | c954bb5600e39f2cc19a96bcbb912ac694b3c16a (patch) | |
| tree | f233980fe76663f29748f604227900985e9d0779 /Makefile.dev | |
| parent | 9165bd2489842af64dbe098ed5906fe69e687bfe (diff) | |
Makefile.install: fix the install of plugin cmi
Now that the plugins are packed, a plugin forms now a unique
compilation unit, and we only need to install the main cmi file of
this plugin (foo_plugin.cmi).
Btw, better variable names (e.g. OMEGACMO instead of OMEGACMA) and
some other cleanup in Makefile.common (no more INITPLUGINS variable,
for instance).
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 f35b861c1..26092e8dc 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -187,16 +187,16 @@ EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO)) CCVO:= DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO)) -omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA) -micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT) -setoid_ring: $(RINGVO) $(RINGCMA) -nsatz: $(NSATZVO) $(NSATZCMA) -extraction: $(EXTRACTIONCMA) -fourier: $(FOURIERVO) $(FOURIERCMA) -funind: $(FUNINDCMA) $(FUNINDVO) -cc: $(CCVO) $(CCCMA) -rtauto: $(RTAUTOVO) $(RTAUTOCMA) -btauto: $(BTAUTOVO) $(BTAUTOCMA) +omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO) +micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) +setoid_ring: $(RINGVO) $(RINGCMO) +nsatz: $(NSATZVO) $(NSATZCMO) +extraction: $(EXTRACTIONCMO) +fourier: $(FOURIERVO) $(FOURIERCMO) +funind: $(FUNINDCMO) $(FUNINDVO) +cc: $(CCVO) $(CCCMO) +rtauto: $(RTAUTOVO) $(RTAUTOCMO) +btauto: $(BTAUTOVO) $(BTAUTOCMO) .PHONY: omega micromega setoid_ring nsatz extraction .PHONY: fourier funind cc rtauto btauto |