From 0eb20167b2ebf5ea3c9ec380acb78c6593df032a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Tue, 28 Sep 2021 12:35:42 +0200 Subject: [PATCH] [server] In states, fixes the array synchronization via [update] and [remove]. --- src/plugins/server/states.ml | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/src/plugins/server/states.ml b/src/plugins/server/states.ml index 04bb0f80b73..08317ce24c1 100644 --- a/src/plugins/server/states.ml +++ b/src/plugins/server/states.ml @@ -209,18 +209,14 @@ let reload array = let update array k = let m = content array in if not m.cleared then - begin - m.updates <- Kmap.add (array.key k) (Add k) m.updates ; - Request.emit array.signal ; - end + m.updates <- Kmap.add (array.key k) (Add k) m.updates ; + Request.emit array.signal let remove array k = let m = content array in if not m.cleared then - begin - m.updates <- Kmap.add (array.key k) Remove m.updates ; - Request.emit array.signal ; - end + m.updates <- Kmap.add (array.key k) Remove m.updates ; + Request.emit array.signal let signal array = array.signal -- GitLab