Oh, so you guys do not use the tools/merge_pull_request.sh script to merge PRs?
- Henry On Thu, Jan 15, 2015 at 6:45 AM, Robert Metzger <rmetz...@apache.org> wrote: > Hi, > I think I remember something like this. I don't really use the tool. > Since I'm using the zsh I always know in which branch I am, so its no big > deal if the tool leaves me in a detached branch. > > Maybe we can think about removing the tool from the repo .. I don't know > anybody using it. > > On Thu, Jan 15, 2015 at 2:33 AM, Henry Saputra <henry.sapu...@gmail.com> > wrote: > >> Hi All, >> >> In the merge tool python, the command "git rev-parse HEAD" actually >> returns you to detached HEAD state after merging PR. >> >> Anyone else seen this behavior? >> >> >> - Henry >>
