chiark / gitweb /
dgit: split brain reorg: Rename $made_split_brain
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Thu, 6 Jun 2019 15:28:57 +0000 (16:28 +0100)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Fri, 28 Jun 2019 11:45:38 +0000 (12:45 +0100)
commitb088a2a398b660f125ab01ae1352c8a094141f51
tree552360f71b92df61abf95b488d519d03e5d39cfd
parentb4195a2465d892f7bf79fba55f169255a2768ada
dgit: split brain reorg: Rename $made_split_brain

This variable is not technnically necessary any more.  But tracking
this means if we introduce bugs which mean that we didn't do the split
brain work, we will get much saner misbehaviour: a crash.

Signed-off-by: Ian Jackson <ijackson@chiark.greenend.org.uk>
dgit