From 3c291f9424dbf78ed508902c1da0fa15938cdd20 Mon Sep 17 00:00:00 2001
From: Nicola Soranzo <nicola.soranzo@earlham.ac.uk>
Date: Tue, 9 Feb 2021 11:54:32 +0000
Subject: [PATCH] Get latest pull request labels

`github.event.pull_request.labels` has often outdated content.

Also drop broken debug statements.
---
 .github/workflows/maintenance_bot.yaml | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/maintenance_bot.yaml b/.github/workflows/maintenance_bot.yaml
index e5ca98a52a6..11f128baf02 100644
--- a/.github/workflows/maintenance_bot.yaml
+++ b/.github/workflows/maintenance_bot.yaml
@@ -10,13 +10,21 @@ jobs:
     env:
       MILESTONE_NUMBER: 19
     steps:
-      - name: Debug
-        run: |
-          echo "Pull request: ${{ toJSON(github.event.pull_request) }}"
-          echo "Pull request labels: ${{ toJSON(github.event.pull_request.labels.*.name) }}"
-          echo "Joined labels: ${{ join(github.event.pull_request.labels.*.name, ', ') }}"
+      - name: Get latest pull request labels
+        id: get_pr_labels
+        uses: actions/github-script@v3
+        with:
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+          script: |
+            const response = await github.issues.listLabelsOnIssue({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              issue_number: context.issue.number,
+            });
+            console.log(response);
+            return response.data;
       - name: Add area labels
-        if: ${{ ! contains(join(github.event.pull_request.labels.*.name, ', '), 'area/') }}
+        if: ${{ ! contains(join(fromJSON(steps.get_pr_labels.outputs.result).*.name, ', '), 'area/') }}
         uses: actions/labeler@main
         with:
           repo-token: "${{ secrets.GITHUB_TOKEN }}"