summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorBen Sima <ben@bsima.me>2024-04-02 00:35:01 -0400
committerBen Sima <ben@bsima.me>2024-04-03 16:18:12 -0400
commitde108b83248b4ab43c4d40b154583f9a9f0e6c1a (patch)
tree24b5d5a76dec267929c8335b29639185a5d9b24a
parentdecc676e917664fabf90b06cf9fc29d236a416da (diff)
Update comment to CI script
It got out of sync with the code even within commit 7597d51ed4c866f596fb690d4d53d70bc01181b4, I dunno how I let that happen.
-rwxr-xr-xBiz/Ide/hooks/pre-push7
1 files changed, 5 insertions, 2 deletions
diff --git a/Biz/Ide/hooks/pre-push b/Biz/Ide/hooks/pre-push
index 16f11d1..eccd4cd 100755
--- a/Biz/Ide/hooks/pre-push
+++ b/Biz/Ide/hooks/pre-push
@@ -3,8 +3,11 @@
# A simple ci that saves its results in a git note, formatted according to
# RFC-2822, more or less.
#
-# To run this manually, exec the script. It will expect to read a line of
-# inputs, you can just enter 'HEAD' and it will
+# To run this manually, exec the script. It will by default run the tests for
+# HEAD, whatever you currently have checked out.
+#
+# It would be cool to use a zero-knowledge proof mechanism here to prove that
+# so-and-so ran the tests, but I'll have to research how to do that.
#
##
set -uo pipefail