From 157fe05a893584c9847e26a42fbe90b063c3b54e Mon Sep 17 00:00:00 2001
From: David Tolnay <dtolnay@gmail.com>
Date: Sat, 4 Jun 2022 16:47:13 -0700
Subject: [PATCH] Print git push command at end of update-revs.sh

---
 scripts/update-revs.sh | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/scripts/update-revs.sh b/scripts/update-revs.sh
index 8243e1d..3fd1707 100755
--- a/scripts/update-revs.sh
+++ b/scripts/update-revs.sh
@@ -8,6 +8,7 @@ if ! git diff-index --quiet HEAD; then
 fi
 
 base=$(git rev-parse HEAD)
+push=()
 
 for rev in 1.{0..70}.0 stable beta nightly; do
     echo "Updating $rev branch"
@@ -17,6 +18,7 @@ for rev in 1.{0..70}.0 stable beta nightly; do
     git add action.yml
     git commit --quiet --message "toolchain: $rev"
     git checkout --quiet -b $rev
+    push+=("$rev:refs/heads/$rev")
 done
 
 for tool in clippy miri; do
@@ -27,6 +29,9 @@ for tool in clippy miri; do
     git add action.yml
     git commit --quiet --message "components: $tool"
     git checkout --quiet -b $tool
+    push+=("$tool:refs/heads/$tool")
 done
 
 git checkout --quiet "$base"
+
+echo "git push origin --force-with-lease ${push[@]}"