From fe3b05ff00eeb4d320d76a491e9e4a117dfa5f20 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 29 Nov 2023 11:07:41 +0100
Subject: [PATCH] Do not listen for label changes

---
 .github/workflows/ci.yml | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 063952583244..8a38a58607df 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -6,7 +6,6 @@ on:
     tags:
       - '*'
   pull_request:
-    types: [opened, synchronize, reopened, labeled]
   merge_group:
   schedule:
     - cron: '0 7 * * *'  # 8AM CET/11PM PT
@@ -38,12 +37,6 @@ jobs:
       LEAN_SPECIAL_VERSION_DESC: ${{ steps.set-release.outputs.LEAN_SPECIAL_VERSION_DESC }}
       RELEASE_TAG: ${{ steps.set-release.outputs.RELEASE_TAG }}
 
-    # Skip everything if a label other than `full-ci` was added
-    # (By skipping the configure job, all other jobs will be skipped as well)
-    # TODO: Double check that the pr release workflow will not be triggered
-    # TODO: Maybe we can trigger the PR release from this workflow instead? Might be cleaner.
-    if: github.event_name != 'label' || github.event.label.name == 'full-ci'
-
     steps:
       - name: Run quick CI?
         id: set-quick