diff --git a/src/plugins/metrics/dune b/src/plugins/metrics/dune index 1fd41b8a7a56115816fbb72dd0d3abb085d8c719..9d4deca66b4275bc8d548d778c75582d99714f68 100644 --- a/src/plugins/metrics/dune +++ b/src/plugins/metrics/dune @@ -12,22 +12,8 @@ ( library (name metrics) (public_name frama-c-metrics.core) - (modules metrics metrics_parameters css_html metrics_base metrics_acsl - metrics_cabs metrics_cilast metrics_coverage - register) (flags -open Frama_c_kernel :standard -w -9) (libraries frama-c.kernel frama-c-eva.core frama-c-server.core) ) (plugin (optional) (name metrics) (libraries frama-c-metrics.core) (site (frama-c plugins))) - -( library - (name metrics_gui) - (public_name frama-c-metrics.gui) - (optional) - (modules metrics_gui_panels register_gui) - (flags -open Frama_c_kernel -open Frama_c_gui -open Metrics :standard -w -9) - (libraries metrics frama-c.kernel frama-c.gui) -) - -(plugin (optional) (name metrics) (libraries frama-c-metrics.gui) (site (frama-c plugins_gui))) diff --git a/src/plugins/metrics/gui/dune b/src/plugins/metrics/gui/dune new file mode 100644 index 0000000000000000000000000000000000000000..b13e820cbd9581362901a6efe33adafcc335dcfa --- /dev/null +++ b/src/plugins/metrics/gui/dune @@ -0,0 +1,10 @@ +( library + (name metrics_gui) + (public_name frama-c-metrics.gui) + (optional) + (modules metrics_gui_panels register_gui) + (flags -open Frama_c_kernel -open Frama_c_gui -open Metrics :standard -w -9) + (libraries frama-c.kernel frama-c.gui frama-c-metrics.core) +) + +(plugin (optional) (name metrics-gui) (libraries frama-c-metrics.gui) (site (frama-c plugins_gui))) diff --git a/src/plugins/metrics/metrics_gui_panels.ml b/src/plugins/metrics/gui/metrics_gui_panels.ml similarity index 100% rename from src/plugins/metrics/metrics_gui_panels.ml rename to src/plugins/metrics/gui/metrics_gui_panels.ml diff --git a/src/plugins/metrics/metrics_gui_panels.mli b/src/plugins/metrics/gui/metrics_gui_panels.mli similarity index 100% rename from src/plugins/metrics/metrics_gui_panels.mli rename to src/plugins/metrics/gui/metrics_gui_panels.mli diff --git a/src/plugins/metrics/register_gui.ml b/src/plugins/metrics/gui/register_gui.ml similarity index 100% rename from src/plugins/metrics/register_gui.ml rename to src/plugins/metrics/gui/register_gui.ml diff --git a/src/plugins/metrics/register_gui.mli b/src/plugins/metrics/gui/register_gui.mli similarity index 100% rename from src/plugins/metrics/register_gui.mli rename to src/plugins/metrics/gui/register_gui.mli