Skip to content

Commit

Permalink
chore: check-prelude also for Std
Browse files Browse the repository at this point in the history
  • Loading branch information
TwoFX committed Oct 18, 2024
1 parent f2ac0d0 commit 187f4af
Showing 1 changed file with 5 additions and 3 deletions.
8 changes: 5 additions & 3 deletions .github/workflows/check-prelude.yml
Original file line number Diff line number Diff line change
Expand Up @@ -11,16 +11,18 @@ jobs:
with:
# the default is to use a virtual merge commit between the PR and master: just use the PR
ref: ${{ github.event.pull_request.head.sha }}
sparse-checkout: src/Lean
sparse-checkout: |
src/Lean
src/Std
- name: Check Prelude
run: |
failed_files=""
while IFS= read -r -d '' file; do
if ! grep -q "^prelude$" "$file"; then
failed_files="$failed_files$file\n"
fi
done < <(find src/Lean -name '*.lean' -print0)
done < <(find src/Lean src/Std -name '*.lean' -print0)
if [ -n "$failed_files" ]; then
echo -e "The following files should use 'prelude':\n$failed_files"
exit 1
fi
fi

0 comments on commit 187f4af

Please sign in to comment.