updated for version 7.0213
diff --git a/src/gui_gtk_x11.c b/src/gui_gtk_x11.c
index 8e66d33..04f1372 100644
--- a/src/gui_gtk_x11.c
+++ b/src/gui_gtk_x11.c
@@ -3198,12 +3198,23 @@
if (!showit != !gtk_notebook_get_show_tabs(GTK_NOTEBOOK(gui.tabline)))
{
+ /* Note: this may cause a resize event */
gtk_notebook_set_show_tabs(GTK_NOTEBOOK(gui.tabline), showit);
update_window_manager_hints();
}
}
/*
+ * Return TRUE when tabline is displayed.
+ */
+ int
+gui_mch_showing_tabline(void)
+{
+ return gui.tabline != NULL
+ && gtk_notebook_get_show_tabs(GTK_NOTEBOOK(gui.tabline));
+}
+
+/*
* Update the labels of the tabline.
*/
void