Set PANE_STYLECHANGED when user options change, from Josh Cooper in

GitHub issue 4825.
This commit is contained in:
nicm
2026-01-22 07:42:30 +00:00
parent 26aacd0e32
commit 818745a605

View File

@@ -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);