mirror of
https://github.com/git/git.git
synced 2024-11-24 10:26:17 +08:00
git-gui: Delete branches with 'git branch -D' to clear config
If we are deleting a local branch from refs/heads/ we need to make sure any associated configuration stored in .git/config is also removed (such as branch.$name.remote and branch.$name.merge). The easiest way to do this is to use git-branch as that automatically will look for and delete configuration keys as necessary. Signed-off-by: Shawn O. Pearce <spearce@spearce.org>
This commit is contained in:
parent
fe70225dc7
commit
76bb40cde0
@ -127,7 +127,7 @@ method _delete {} {
|
|||||||
foreach i $to_delete {
|
foreach i $to_delete {
|
||||||
set b [lindex $i 0]
|
set b [lindex $i 0]
|
||||||
set o [lindex $i 1]
|
set o [lindex $i 1]
|
||||||
if {[catch {git update-ref -d "refs/heads/$b" $o} err]} {
|
if {[catch {git branch -D $b} err]} {
|
||||||
append failed " - $b: $err\n"
|
append failed " - $b: $err\n"
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user