Display the PR title in merge_pr

Author: branfosj

easybuild/tools/github.py

@@ -1381,6 +1381,7 @@ def merge_pr(pr):
 
     msg = "\n%s/%s PR #%s was submitted by %s, " % (pr_target_account, pr_target_repo, pr, pr_data['user']['login'])
     msg += "you are using GitHub account '%s'\n" % github_user
+    msg += "\nPR title: %s\n\n" % pr_data['title']
     print_msg(msg, prefix=False)
     if pr_data['user']['login'] == github_user:
         raise EasyBuildError("Please do not merge your own PRs!")