From 8d548081f63dd87df31684b33c804c050c55460c Mon Sep 17 00:00:00 2001
From: David Holland <dholland@galois.com>
Date: Thu, 24 Oct 2024 17:38:11 -0400
Subject: [PATCH] Provisionally revert mergify.yml.

(to what it was before the label-related changes)

This is an experiment to see what happens in the CI run and not
expected to be merged.
---
 .github/mergify.yml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/.github/mergify.yml b/.github/mergify.yml
index 3b6462574a..a73b6cde35 100644
--- a/.github/mergify.yml
+++ b/.github/mergify.yml
@@ -8,7 +8,7 @@ pull_request_rules:
     conditions:
       - "#approved-reviews-by>=1"
       - check-success=mergify
-      - label="PR: ready to merge"
+      - label=ready-to-merge
     actions:
       update: {}
       queue:
@@ -17,12 +17,11 @@ pull_request_rules:
   - name: Delete head branch after merge
     conditions:
       - merged
-      # disabled October 2024
-      # - label!=keep-branch-after-merge
+      - label!=keep-branch-after-merge
     actions:
       delete_head_branch: {}
   - name: Keep pull requests with keep-updated label updated
     conditions:
-      - label="PR: keep updated"
+      - label=keep-updated
     actions:
       update: {}