dunecontrol fails when a branch with name 'dune.module' is created.

This is probably the best bug I have seem in my entire time with DUNE.

See mailing list discussion: https://lists.dune-project.org/pipermail/dune-devel/2022-October/002961.html

added bug buildsystem labels

@andreas.dedner , @simon.praetorius: Please add the discussion from the mainling list here.

added bug-of-the-year label

removed bug label

I have in dune-localfunction for some reason the same problem. There was an old branch "bugfix/dune.module" that is somewhere in the .git folder referenced. But it is not anymore in the online repository (already deleted or renamed). And I cannot delete it in by local repository since it was never checked out. How to get rid of this locally?

I have found a solution myself:

git remote prune origin [--dry-run]

to delete all remote branches from origin that do not exist anymore

git pull --prune should also work.

mentioned in merge request !1184 (merged)

changed the description

closed with merge request !1184 (merged)

mentioned in commit 5598f298

mentioned in issue #384