From f27667dc33e7ff9a679224e7f68270dde1079f49 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 3 Jun 2020 13:16:48 +0200
Subject: [PATCH] [server] kernel.properties array: new column for the names of
properties.
---
src/plugins/server/kernel_properties.ml | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 968e8fef88d..9d6e9e55ed9 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -227,6 +227,11 @@ let () = States.column ~model ~name:"kind"
~data:(module PropKind)
~get:(fun ip -> ip) ()
+let () = States.column ~model ~name:"names"
+ ~descr:(Md.plain "Names")
+ ~data:(module Jstring.Jlist)
+ ~get:Property.get_names ()
+
let () = States.column ~model ~name:"status"
~descr:(Md.plain "Status")
~data:(module PropStatus)
--
GitLab