Yeap. I just merged it with Github's "Squash and Merge" button. I also wonder which is better but I feel like both are ok but the disadvantage of Github button is that we couldn't cherry-pick to another branch automatically.
I talked to Jeff about the same issue and we concluded both would be ok. Hope this helps, Jongyoul 2022년 3월 31일 (목) 오후 5:33, Philipp Dallig <philipp.dal...@gmail.com>님이 작성: > Hi Jeff and Jongyoul, > it seems that you have changed the way of merging pull requests into the > Zeppelin master branch. > > The following pull request > (https://github.com/apache/zeppelin/pull/4332) looks great in GitHub > (marked as merged) and in the commit histroy > ( > https://github.com/apache/zeppelin/commit/4b60f08bd0ad241a7b197d7165abbb7c066ec979) > > with a link into the Apache JIRA. > > How did you achieve this? > > I failed with the pull request > https://github.com/apache/zeppelin/pull/4337 > > I merged the last pull requests with the `./dev/merge_zeppelin_pr.py` > script, but this script closes the pull requests, which does not look > good in GitHub. > > Best Regards > Philipp > > -- 이종열, Jongyoul Lee, 李宗烈 http://madeng.net
