build: remove Ready to Merge label when PR is merged

---
type: pre_commit_static_analysis_report
description: Results of running static analysis checks when committing changes.
report:
  - task: lint_filenames
    status: passed
  - task: lint_editorconfig
    status: passed
  - task: lint_markdown
    status: na
  - task: lint_package_json
    status: na
  - task: lint_repl_help
    status: na
  - task: lint_javascript_src
    status: na
  - task: lint_javascript_cli
    status: na
  - task: lint_javascript_examples
    status: na
  - task: lint_javascript_tests
    status: na
  - task: lint_javascript_benchmarks
    status: na
  - task: lint_python
    status: na
  - task: lint_r
    status: na
  - task: lint_c_src
    status: na
  - task: lint_c_examples
    status: na
  - task: lint_c_benchmarks
    status: na
  - task: lint_c_tests_fixtures
    status: na
  - task: lint_shell
    status: na
  - task: lint_typescript_declarations
    status: passed
  - task: lint_typescript_tests
    status: na
  - task: lint_license_headers
    status: passed
---

Author: Planeshifter

.github/workflows/labeler.yml

@@ -138,6 +138,25 @@ jobs:
               console.log( 'Error removing label: %s', error.message );
             }
 
+      # Remove "Ready To Merge" label when PR is merged:
+      - name: 'Remove "Ready To Merge" label if PR is merged'
+        if: ${{ github.event.action == 'closed' && github.event.pull_request.merged == true }}
+        # Pin action to full length commit SHA
+        uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.0.0
+        with:
+          github-token: ${{ secrets.STDLIB_BOT_PAT_REPO_WRITE }}
+          script: |
+            try {
+              await github.rest.issues.removeLabel({
+                'owner': context.repo.owner,
+                'repo': context.repo.repo,
+                'issue_number': context.payload.pull_request.number,
+                'name': 'Ready To Merge'
+              })
+            } catch ( error ) {
+              console.log( 'Error removing label: %s', error.message );
+            }
+
       # Remove "Needs Review" and "Needs Changes" labels when "Ready To Merge" is assigned:
       - name: 'Remove "Needs Review" and "Needs Changes" labels when "Ready To Merge" is assigned'
         if: ${{ github.event.action == 'labeled' && github.event.label.name == 'Ready To Merge' }}