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:"