From 0b913432097d319207f2bf44757a8b8601dc6fe1 Mon Sep 17 00:00:00 2001 From: Neves-P Date: Tue, 11 Jun 2024 16:41:46 +0200 Subject: [PATCH] merged is a Bool (?) --- eessi_bot_event_handler.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/eessi_bot_event_handler.py b/eessi_bot_event_handler.py index f60f91b..3d6dc6d 100644 --- a/eessi_bot_event_handler.py +++ b/eessi_bot_event_handler.py @@ -621,11 +621,11 @@ def handle_pull_request_closed_event(self, event_info, pr): action = request_body['action'] merged = request_body['pull_request']['merged'] - if merged == 'True': + if merged: self.log("PR merged: scanning directories used by PR") self.log(f"pull_request event with action '{action}' and merged '{merged}' will be handled") else: - self.log(f"Action '{action}' not handled as merged is '{merged}'") + self.log(f"Action '{action}' not handled as 'merged' is '{merged}'") return # at this point we know that we are handling a new merge # NOTE: Permissions to merge are already handled through GitHub, we