Dead branches deletion? [Re: [expr]-fix [jk-expr-committed] Fixcrash on C++ DW_AT_name "".]

[Jan Kratochvil <jan dot kratochvil at redhat dot com>]

On Tue, 17 Mar 2009 22:20:44 +0100, Tom Tromey wrote:
> (Though I see on the wiki that this is listed as a dead branch... is
> that accurate?)

Dodji suggested one can delete the remote GIT branches by:

	git push origin :branch-to-delete

(it worked for me when I was fixing up `archer-jankratochvil-fedora-merge')

Is there any reason to keep the `Dead Branches' wiki section and not just
delete those branches to make the `git branch -r | grep archer' listing
easier?  Although CVS can also delete the branches while is is usual to keep
them in the repositories.

Or maybe just delete completely empty branches (like my
archer-jankratochvil-fedora) and keep the real but obsolete ones for
historical reasons?


Thanks,
Jan