From 502b80ad817309412d60f1f5f1cbc40371e54584 Mon Sep 17 00:00:00 2001
From: Simon Michael <simon@joyful.com>
Date: Sat, 27 May 2023 12:47:32 -1000
Subject: [PATCH] ;dev: push: ensure git's pager doesn't stop progress

---
 tools/push | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/tools/push b/tools/push
index ea9bbe170..dee348e4a 100755
--- a/tools/push
+++ b/tools/push
@@ -36,6 +36,9 @@ ciwait() {
     sleep $MAINPUSHDELAY
 }
 
+# ensure git's use of pager doesn't stop progress
+export PAGER=cat
+
 echo "latest local commits are:"
 gitlog
 echo "force-pushing $LOCALBRANCH to $REMOTE/$REMOTECIBRANCH"