Fixing issues found in review of 2023-01-30 <https://github.com/ravenbrook/mps/pull/117#issuecomment-1408484708>: clarifying leader comment. adding usage. referencing shellcheck manual.

This commit is contained in:
Richard Brooksby 2023-01-30 16:49:41 +00:00
parent 2a64952735
commit 0aa891e6cf

View file

@ -9,11 +9,19 @@
# It can be invoked from the command line of from Continuous
# Integration scripts.
#
# The script excludes .git because it contains default Git Hooks
# installed by git that trigger shellcheck.
# Usage (in the root directory of the MPS tree)::
#
# tool/check-shell-scripts
#
# This script excludes some directories from checking:
#
# - It excludes .git because Git installs shell scripts (the default
# "Git Hooks") that provoke warnings from shellcheck, and we can't
# fix them.
#
# - It excludes tool/autoconf because those scripts are part of GNU
# autoconf, provoke warnings from shellcheck, and we can't fix them.
#
# The script ignores tool/autoconf because those scripts are part of
# GNU autoconf and not under our control.
find . -path './.git' -prune -o \
-path './tool/autoconf' -prune -o \
@ -33,7 +41,9 @@ find . -path './.git' -prune -o \
# A. REFERENCES
#
# [None]
# [Shellcheck] "shellcheck - Shell script analysis tool" version
# 0.8.0; Vidar Holen and contributors;
# <https://github.com/koalaman/shellcheck/blob/e5ad4cf420a7f7b8e5eaac872b14a1619051cf10/shellcheck.1.md>.
#
#
# B. DOCUMENT HISTORY