git question

[Edward Z. Yang]

Get to the commit you want to edit, then

    cd utils/haddock
    git checkout 073d899a8f94ddec698f617a38d3420160a7fd0b
    cd ../..
    git commit --amend -a

Excerpts from Simon Peyton Jones via ghc-devs's message of 2016-09-30 10:47:24 +0000:
> Friends
> I have a batch of several commits lined up on my local machine, validated, and ready to push to the master.
> But one seems to have accidentally got
> 
> diff --git a/utils/haddock b/utils/haddock
> 
> index 073d899..a3309e7 160000
> 
> --- a/utils/haddock
> 
> +++ b/utils/haddock
> 
> @@ -1 +1 @@
> 
> -Subproject commit 073d899a8f94ddec698f617a38d3420160a7fd0b
> 
> +Subproject commit a3309e797c42dae9bccdeb17ce52fcababbaff8a
> I did not want to meddle with Haddock.
> Question: how can I remove this change from my commit?  I know how to do git rebase –interactive, and I can aske to “edit” that commit… but what then?
> Thanks
> Simon