Hi, during our discussion on how to close the Github pull requests, Henry suggested to create a script for merging pull requests ( http://apache-flink-incubator-mailing-list-archive.1008284.n3.nabble.com/Admin-access-to-github-com-apache-incubator-flink-tp160p246.html ).
I found a nice python script in the Spark repository that does exactly this. It assumes exactly our setup with the GitHub integration and can even automatically close the JIRA if its ID is contained in the pull request title. This shows how the tool works: https://gist.github.com/rmetzger/cf4d2eba940483d704a2 So committers have to basically enter the pull request ID, press "y" three times and everything is done. (You can still check if everything is correct in another window). What do you think? Should I merge it into the "tools" directory? Robert
