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).

0 files changed, 0 insertions, 0 deletions