From 756fd6674596562d65ba2301a482d26de3a99947 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 20 Mar 2025 13:16:43 +0100
Subject: [PATCH] chore: CI: relax check-stage0 check

---
 .github/workflows/check-stage0.yml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/.github/workflows/check-stage0.yml b/.github/workflows/check-stage0.yml
index 6186e47df9..abef1d38df 100644
--- a/.github/workflows/check-stage0.yml
+++ b/.github/workflows/check-stage0.yml
@@ -20,9 +20,7 @@ jobs:
 
     - name: Identify stage0 changes
       run: |
-        git diff "${BASE:-HEAD^}..HEAD" --name-only -- stage0 |
-          grep -v -x -F $'stage0/src/stdlib_flags.h\nstage0/src/lean.mk.in' \
-          > "$RUNNER_TEMP/stage0" || true
+        git diff "${BASE:-HEAD^}..HEAD" --name-only -- stage0/stdlib > "$RUNNER_TEMP/stage0" || true
         if test -s "$RUNNER_TEMP/stage0"
         then
           echo "CHANGES=yes" >> "$GITHUB_ENV"