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"