From 8fe03d20268457ed52f8aa6dab519b9b4694c949 Mon Sep 17 00:00:00 2001
From: Peter Evans <peter-evans@users.noreply.github.com>
Date: Tue, 23 Jul 2019 11:26:05 +0900
Subject: [PATCH] Add explanation for ignoring the push event on deleted
branches
---
create-pull-request.py | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/create-pull-request.py b/create-pull-request.py
index 06b6150..bf2105e 100755
--- a/create-pull-request.py
+++ b/create-pull-request.py
@@ -16,6 +16,10 @@ def get_github_event(github_event_path):
def ignore_event(github_event):
# Ignore push events on deleted branches
+ # The event we want to ignore occurs when a PR is created but the repository owner decides
+ # not to commit the changes. They close the PR and delete the branch. This creates a
+ # "push" event that we want to ignore, otherwise it will create another branch and PR on
+ # the same commit.
deleted = "{deleted}".format(**github_event)
if deleted == "True":
print("Ignoring delete branch event.")