From 195db8833751bb4a75a3cdf8bcaabed267cb13de Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 31 May 2022 12:45:49 +0200
Subject: [PATCH] [metrics] move gui to subdir
---
src/plugins/metrics/dune | 14 --------------
src/plugins/metrics/gui/dune | 10 ++++++++++
.../metrics/{ => gui}/metrics_gui_panels.ml | 0
.../metrics/{ => gui}/metrics_gui_panels.mli | 0
src/plugins/metrics/{ => gui}/register_gui.ml | 0
src/plugins/metrics/{ => gui}/register_gui.mli | 0
6 files changed, 10 insertions(+), 14 deletions(-)
create mode 100644 src/plugins/metrics/gui/dune
rename src/plugins/metrics/{ => gui}/metrics_gui_panels.ml (100%)
rename src/plugins/metrics/{ => gui}/metrics_gui_panels.mli (100%)
rename src/plugins/metrics/{ => gui}/register_gui.ml (100%)
rename src/plugins/metrics/{ => gui}/register_gui.mli (100%)
diff --git a/src/plugins/metrics/dune b/src/plugins/metrics/dune
index 1fd41b8a7a5..9d4deca66b4 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 00000000000..b13e820cbd9
--- /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
--
GitLab