[tools] master update

[Mark J. Cox]

The branch master has been updated
       via  1a4ebc8a908344ddff8121eb664cf9f29e60d89a (commit)
       via  aef3a920ed35ecf2d539c02ac3a77f45a82c8c2f (commit)
      from  b51efa70790d498f07e221348dc3e07f3b2889bc (commit)


- Log -----------------------------------------------------------------
commit 1a4ebc8a908344ddff8121eb664cf9f29e60d89a
Author: Mark J. Cox <mark at awe.com>
Date:   Fri Feb 7 11:14:22 2020 +0000

    PRs are issues but let's be clear

commit aef3a920ed35ecf2d539c02ac3a77f45a82c8c2f
Author: Mark J. Cox <mark at awe.com>
Date:   Fri Feb 7 11:00:40 2020 +0000

    Add a notification when ready to merge
    fixes #52

-----------------------------------------------------------------------

Summary of changes:
 github-approve-label-workflow/github-approve-label-workflow.py | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/github-approve-label-workflow/github-approve-label-workflow.py b/github-approve-label-workflow/github-approve-label-workflow.py
index 93ffd72..ecacdf5 100644
--- a/github-approve-label-workflow/github-approve-label-workflow.py
+++ b/github-approve-label-workflow/github-approve-label-workflow.py
@@ -59,6 +59,13 @@ def movelabeldonetoready(issue):
     res = requests.post(url, data=json.dumps(newlabel), headers=headers)
     if (res.status_code != 200):
         print("Error adding label", res.status_code, res.content)
+        return
+    newcomment = {"body":"This pull request is ready to merge"}
+    url = api_url + "/issues/" + str(issue) + "/comments"
+    res = requests.post(url, data=json.dumps(newcomment), headers=headers)
+    if (res.status_code != 201):
+        print("Error adding comment", res.status_code, res.content)
+        return
 
 # Check through an issue and see if it's a candidate for moving