Johannes Schauer writes ("Re: Bug#800060: dgit push failed with checksum
mismatch"):
> Is it hard to delete the dgit repository for botch? I did a number of test
> commits to diagnose this problem and would like to start the git history from
> scratch)I'm afraid that the git repository is deliberately not deletable. You can make an alternative history and do `git merge -s ours', though, which will often make git descend the interesting branch. Ian.
