From 748e4e8e5d8c02bc7c7d54e286bd691a8c0c900d Mon Sep 17 00:00:00 2001
From: Simon Michael <simon@joyful.com>
Date: Tue, 6 Jun 2023 20:35:22 -1000
Subject: [PATCH] ;dev: comment

---
 tools/push | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/push b/tools/push
index dee348e4a..f53427a9b 100755
--- a/tools/push
+++ b/tools/push
@@ -36,7 +36,7 @@ ciwait() {
     sleep $MAINPUSHDELAY
 }
 
-# ensure git's use of pager doesn't stop progress
+# ensure git's output paging doesn't stop progress
 export PAGER=cat
 
 echo "latest local commits are:"