Makefile.dynamic should always write to $(DESTDIR)
ID0000528: This issue was created automatically from Mantis Issue 528. Further discussion may take place here.
|ID0000528||Frama-C||Kernel > Makefile||public||2010-07-04||2014-02-12|
|Reporter||Jonathan-Christofer Demay||Assigned To||signoles||Resolution||fixed|
|Product Version||Frama-C Boron-20100401||Target Version||-||Fixed in Version||Frama-C Carbon-20101201-beta1|
When a dynamic plugin is being built in a sandbox, the install process should always write to $(DESTDIR).
This is already the case for everything that go into $(BINDIR), but not into $(PLUGIN_INSTALL_DIR)
The attached patch fixes that.
However, the part that updates 'known_plugins.ac' is also a problem for the same reason. I haven't figured out yet what to do with it, so as of now it is just disabled.