From 2d3f3f01270a47bed15db774b577b22a9c9c8d9e Mon Sep 17 00:00:00 2001 From: Johannes Sixt Date: Fri, 18 Jul 2025 22:49:21 +0200 Subject: [PATCH] gitk: remove header of now empty section "General options" An earlier commit remove the only option that was available under "General options". We don't need the header for the empty section. Signed-off-by: Johannes Sixt --- gitk | 2 -- 1 file changed, 2 deletions(-) diff --git a/gitk b/gitk index c6f4758a6c..427a8a96c9 100755 --- a/gitk +++ b/gitk @@ -11707,8 +11707,6 @@ proc prefspage_general {notebook} { pack configure $page.webbrowserf.l -padx 10 grid x $page.webbrowserf $page.webbrowser -sticky ew - ttk::label $page.lgen -text [mc "General options"] -font mainfontbold - grid $page.lgen - -sticky w -pady 10 return $page } -- 2.47.2