PLUGIN_LINK_GUI_OFLAGS not used ?
ID0001145: This issue was created automatically from Mantis Issue 1145. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0001145 | Frama-C | Kernel > Makefile | public | 2012-04-12 | 2014-02-12 |
Reporter | Anne | Assigned To | signoles | Resolution | fixed |
Priority | normal | Severity | minor | Reproducibility | have not tried |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
It seems that the variables PLUGIN_LINK_GUI_BFLAGS and PLUGIN_LINK_GUI_OFLAGS that can be defined in plug-ins Makefile are not used in Makefile.plugin.
In $(TARGET_GUI_CMXS) I managed to change :
$(OCAMLOPT) -o $@ -shared $^
into
$(OCAMLOPT) -o $@ -shared (
(basename $(notdir $@))_OFLAGS)
(
(basename $(notdir $@))_gui_TARGET_GUI_OFLAGS)
$^
to make it work in my plug-in,
but I guess that there are other modifications to do...