From 0aa891e6cfe4d243ac26c8b04a8a826efc349ec9 Mon Sep 17 00:00:00 2001
From: Richard Brooksby <rb@ravenbrook.com>
Date: Mon, 30 Jan 2023 16:49:41 +0000
Subject: [PATCH] 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.

---
 mps/tool/check-shell-scripts | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

diff --git a/mps/tool/check-shell-scripts b/mps/tool/check-shell-scripts
index 735b7e6c257..bbb2fe2c90d 100755
--- a/mps/tool/check-shell-scripts
+++ b/mps/tool/check-shell-scripts
@@ -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