From 1e718187676d7fa3feedff0cb806b673d9042602 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Mon, 20 Sep 2021 08:50:55 -0700
Subject: [PATCH] Add some functionality comments to ci.sh

---
 .github/ci.sh | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/.github/ci.sh b/.github/ci.sh
index 8c09e3c7a..958a1f950 100755
--- a/.github/ci.sh
+++ b/.github/ci.sh
@@ -9,6 +9,11 @@ mkdir -p "$BIN"
 
 is_exe() { [[ -x "$1/$2$EXT" ]] || command -v "$2" > /dev/null 2>&1; }
 
+# The deps() function is primarily used for producing debug output to
+# the CI logging files.  For each platform, it will indicate which
+# shared libraries are needed and if they are present or not.  The
+# '|| true' is used because statically linked binaries will cause
+# ldd (and possibly otool) to exit with a non-zero status.
 deps() {
   case "$RUNNER_OS" in
     Linux) ldd $1 || true ;;
@@ -17,6 +22,8 @@ deps() {
   esac
 }
 
+# Finds the cabal-built '$1' executable and copies it to the '$2'
+# directory.
 extract_exe() {
   exe="$(cabal v2-exec which "$1$EXT")"
   name="$(basename "$exe")"