diff options
| -rwxr-xr-x | Meta/lint-shell-scripts.sh | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Meta/lint-shell-scripts.sh b/Meta/lint-shell-scripts.sh index 37e1efcdb0..0d7f0b8e60 100755 --- a/Meta/lint-shell-scripts.sh +++ b/Meta/lint-shell-scripts.sh @@ -17,6 +17,11 @@ if [ "$#" -eq "0" ]; then else files=() for file in "$@"; do + # Skip ports, like we in the CI case above. + if [[ "${file}" =~ "Ports" ]]; then + continue + fi + if [[ "${file}" == *".sh" && "${file}" != "Base/root/generate_manpages.sh" ]]; then files+=("${file}") fi |