-
Alexander Diewald authored
For each git repository, add the property "remote.origin.prune = true" such that the local copies of deleted remote branches are removed at every fetch from these repositories. Signed-off-by: Alexander Diewald <diewald@fortiss.org>
77d34224