From b790ebab931e27efa91f002ad32f7ce2f0ec9177 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Wed, 4 Jan 2023 11:57:29 +0100
Subject: [PATCH] fix: hide the priority grid in synchronous mode of
rdbgui4sasa
---
tools/rdbg4sasa/gtkgui.ml | 10 ++++++----
1 file changed, 6 insertions(+), 4 deletions(-)
diff --git a/tools/rdbg4sasa/gtkgui.ml b/tools/rdbg4sasa/gtkgui.ml
index 523f0a96..8cffd03a 100644
--- a/tools/rdbg4sasa/gtkgui.ml
+++ b/tools/rdbg4sasa/gtkgui.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 04/01/2023 (at 11:44) by Erwan Jahier> *)
+(* Time-stamp: <modified the 04/01/2023 (at 11:56) by Erwan Jahier> *)
#thread
#require "lablgtk3"
@@ -418,11 +418,13 @@ let custom_daemon p gtext vbox step_button back_step_button round_button
pushbox#set_sensitive enabled
| Synchronous | Distributed | Central | LocCentral ->
- if !daemon_kind = Synchronous then show undo_button
- else hide undo_button;
+ if !daemon_kind = Synchronous then (
+ show undo_button; hide counter_grid
+ ) else (
+ hide undo_button; show counter_grid
+ );
(match !oracle_button_ref with Some b -> show b | None -> ());
show back_step_button; show step_button; show round_button;
- show counter_grid;
if not args.salut_mode then show legitimate_button; (* for the time being *)
hide checkbox_grid; hide pushbox_grid;
in
--
GitLab