From c954bb5600e39f2cc19a96bcbb912ac694b3c16a Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Fri, 24 Jun 2016 01:06:46 +0200
Subject: 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).
---
 Makefile.dev | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'Makefile.dev')

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
-- 
cgit v1.2.3