Skip to content

Commit

Permalink
chore(lint-style.sh): remove duplicate check for case clashes (#15027)
Browse files Browse the repository at this point in the history
The check_case action (run earlier in the same workflow step) runs the same check across the entire repository.
  • Loading branch information
grunweg committed Jul 22, 2024
1 parent d995afc commit 407f293
Showing 1 changed file with 1 addition and 14 deletions.
15 changes: 1 addition & 14 deletions scripts/lint-style.sh
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ set -exo pipefail
# Exceptions are maintained in `scripts/style-exceptions.txt`.
# (Rewriting these checks in Lean is work in progress.)
# 2. The remainder of this shell script
# contains some lints on the global repository.
# contains a lint on the global repository.
#
# TODO: This is adapted from the linter for mathlib3. It should be rewritten in Lean.

Expand All @@ -47,8 +47,6 @@ lake exe lint_style --github

# 2. Global checks on the mathlib repository

# 2.1 Check for executable bit on Lean files

executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"

if [[ -n "$executable_files" ]]
Expand All @@ -57,14 +55,3 @@ then
echo "$executable_files"
exit 1
fi

# 2.2 Check that there are no filenames with the same lower-case reduction

# `uniq -D`: print all duplicate lines
ignore_case_clashes="$(git ls-files | sort --ignore-case | uniq -D --ignore-case)"

if [ -n "${ignore_case_clashes}" ]; then
printf $'The following files have the same lower-case form:\n\n%s\n
Please, make sure to avoid such clashes!\n' "${ignore_case_clashes}"
exit 1
fi

0 comments on commit 407f293

Please sign in to comment.