From 818745a6056fdeb1e761e6c27fb91ea286b2ccbf Mon Sep 17 00:00:00 2001 From: nicm Date: Thu, 22 Jan 2026 07:42:30 +0000 Subject: [PATCH] Set PANE_STYLECHANGED when user options change, from Josh Cooper in GitHub issue 4825. --- options.c | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/options.c b/options.c index bfbec5c7..37160b7a 100644 --- a/options.c +++ b/options.c @@ -1226,6 +1226,10 @@ options_push_changes(const char *name) RB_FOREACH(wp, window_pane_tree, &all_window_panes) wp->flags |= (PANE_STYLECHANGED|PANE_THEMECHANGED); } + if (*name == '@') { + RB_FOREACH(wp, window_pane_tree, &all_window_panes) + wp->flags |= PANE_STYLECHANGED; + } if (strcmp(name, "pane-colours") == 0) { RB_FOREACH(wp, window_pane_tree, &all_window_panes) colour_palette_from_option(&wp->palette, wp->options);