fix: don't comment twice when a pr is closed with comment. #277

This check (that the comment create date and the pull request closed
date are the same) might not be 100% fool-proof. If they are off by one
second, the bot will still comment twice, but that should be unlikely.

changelog.d/20231114_044217_nedbat.rst

@@ -0,0 +1,3 @@
+.. A new scriv changelog fragment.
+
+- Fix: we no longer comment twice on a pull request closed with a comment. #277

openedx_webhooks/github_views.py

@@ -122,6 +122,16 @@ def handle_comment_event(event):
             # for our own comment events.
             pass
 
+        case {
+            "issue": {"closed_at": closed}, 
+            "comment": {"created_at": commented},
+            } if closed == commented:
+
+            # This is a "Close with comment" comment. Don't do anything for the
+            # comment, because we'll also get a "pull request closed" event at
+            # the same time, and it will do whatever we need.
+            pass
+
         case {"issue": {"pull_request": _}}:
             # The comment is on a pull request.  Re-shape the data to conform to
             # a pull request reported by a pull request event, and fire
@@ -132,9 +142,6 @@ def handle_comment_event(event):
             pr["hook_action"] = event["action"]
             return queue_task(pull_request_changed_task, pr)
 
-        case _:
-            pass
-
     return "No thanks", 202