From 5529c958d172397cbdf226658f98b779222e4fdc Mon Sep 17 00:00:00 2001
From: David Tolnay <dtolnay@gmail.com>
Date: Tue, 25 Oct 2022 12:20:58 -0700
Subject: [PATCH] Push same commit as both minor and largest patch
---
scripts/update-revs.sh | 10 +++++++++-
1 file changed, 9 insertions(+), 1 deletion(-)
diff --git a/scripts/update-revs.sh b/scripts/update-revs.sh
index 9fd2b55..9b4e128 100755
--- a/scripts/update-revs.sh
+++ b/scripts/update-revs.sh
@@ -14,12 +14,17 @@ patch_releases=(
)
releases() {
- printf "%s\n" 1.{0..70}{,.0} ${patch_releases[@]} | sort -V
+ printf "%s\n" 1.{0..70}.0 ${patch_releases[@]} | sort -V
}
base=$(git rev-parse HEAD)
push=()
+declare -A minor
+for rev in `releases`; do
+ minor[${rev%.*}]=$rev
+done
+
for rev in `releases` stable beta nightly; do
echo "Updating $rev branch"
git checkout --quiet "$base"
@@ -29,6 +34,9 @@ for rev in `releases` stable beta nightly; do
git commit --quiet --message "toolchain: $rev"
git checkout --quiet -b $rev
push+=("$rev:refs/heads/$rev")
+ if [ ${minor[${rev%.*}]} == $rev ]; then
+ push+=("$rev:refs/heads/${rev%.*}")
+ fi
done
for tool in clippy miri; do