-# * dgit push usually needs to (re)make a pseudomerge. The "first"
-# git-debrebase stripped out the previous pseudomerge and could
-# have remembeed the HEAD. But it's not quite clear what history
-# ought to be preserved and what should be discarded. For now
-# the user will have to tell dgit --overwrite.
-#
-# To fix this, do we need a new push hook for dgit ?
-#