[GitHub] lebeg edited a comment on issue #12784: Improved git reset for CI builds

[GitBox <gi...@apache.org>]

lebeg edited a comment on issue #12784: Improved git reset for CI builds
URL: https://github.com/apache/incubator-mxnet/pull/12784#issuecomment-430982022
 
 
   > As you can see, Jenkins runs git merge 76ae7252a6751275565600d287b7d432b685fd7d and thus creates a temporary commit that merges the PR with the head of master (in case your PR was not rebased). Your command would delete that commit.
   
   This is not true, since after merge is performed `HEAD` points to the merge commit.
   
   > If we execute your git clean (or run PR-head strategy), the HEAD of the PR will be depending on the base of the PR.
   
   This is not true either.
   
   Refer to `git-reset --hard` [documentation](https://git-scm.com/docs/git-reset#git-reset---hard). Without an argument it assumes `HEAD`, with as I've stated previously points to the merge commit.

----------------------------------------------------------------
This is an automated message from the Apache Git Service.
To respond to the message, please log on GitHub and use the
URL above to go to the specific comment.
 
For queries about this service, please contact Infrastructure at:
users@infra.apache.org


With regards,
Apache Git Services