Andor Molnar created ZOOKEEPER-4756:
---------------------------------------
Summary: Merge script should use GitHub api to merge pull requests
Key: ZOOKEEPER-4756
URL: https://issues.apache.org/jira/browse/ZOOKEEPER-4756
Project: ZooKeeper
Issue Type: Improvement
Components: tools
Affects Versions: 3.9.0
Reporter: Andor Molnar
Github merge script (zk-merge-pr.py) is a nice tool which does a lot of
housekeeping tasks when merging a PR including fixing the commit message or
closing the Jira. Merging on the Github UI is also possible, but could lead to
mistakes like leaving the commit message without the Jira id.
Unfortunately when the script merges the PR it does that without Github and
leaving the PR in 'Closed' rather than 'Merged'. This is misleading. Let's
improve the script to use Github API for merging PRs and possibly disable
merging on the Github UI.
Email thread:
[https://lists.apache.org/thread/cbmktklydtlylkybvq6jrx5m4l8b2cm5]
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
