Makefile.dynamic should always write to $(DESTDIR)
ID0000528: This issue was created automatically from Mantis Issue 528. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0000528 | Frama-C | Kernel > Makefile | public | 2010-07-04 | 2014-02-12 |
Reporter | Jonathan-Christofer Demay | Assigned To | signoles | Resolution | fixed |
Priority | normal | Severity | minor | Reproducibility | always |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | Frama-C Carbon-20101201-beta1 |
Description :
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.