On 2015-12-15 at 21:12 Gan Shun <[email protected]> wrote: > Noted. > > If checkpatch shows an error that is actually removed in a later > commit, what do I do?
Unless it's a big pain, use git rebase to fix it up. Using git is a learning process. For something minor, the easiest thing is to: $ git rebase -i some_commit_thats_far_back 'edit' the commit that caused the problem. Now git rebase will stop at that commit and let you do whatever you want. I'd edit the file right there, then do: $ git add -p $ git commit --amend Now the fix is in the right place. But you'll run into conflicts when you finish the rebase: $ git rebase --continue (resolve the conflicts in follow-on commits). This same approach goes for any fixes, whether they are for checkpatch or other stuff. Another approach is to split the commit that did the fixup into multiple commits, then move those commits around. Here's what I posted in another thread: $ git rebase -i some-commit-far-back-enough pick the commit you want to split. change it from "pick" to "edit". take note of the commit hash (will need it later). git will stop there, then you can do whatever you want to that commit. at that point i do: $ git reset HEAD^ (pops off the commit.) $ git add -p (selectively add back in all of the things that should have been in that original commit, but not the things you don't want) $ git commit -c HASH_FROM_THE_COMMIT_ORIGINALLY then add everything else from that commit to a WIP commit: $ git add -p $ git commit -m WIP-fixing-whatever Then finish the git rebase: $ git rebase --continue At this point, all that did was split up a commit into two commits. You could do whatever you want during that 'edit' phase of the rebase, including making more commits. Then you do another rebase -i, and move the WIP-fixing-whatever to the right spot in the history. -- You received this message because you are subscribed to the Google Groups "Akaros" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. For more options, visit https://groups.google.com/d/optout.
