Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix(noir-mirror): don't update .gitrepo on push #4555

Merged
merged 11 commits into from
Feb 13, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 2 additions & 3 deletions .github/workflows/mirror_noir_subrepo.yml
Original file line number Diff line number Diff line change
Expand Up @@ -95,9 +95,8 @@ jobs:
COMMIT=$(git rev-parse HEAD)
# Now push to it with subrepo with computed commit messages
if ./scripts/git-subrepo/lib/git-subrepo push $SUBREPO_PATH --squash --branch=$STAGING_BRANCH; then
# We don't push a commit to aztec anymore so that we can maintain the 'commit' as our last pull branch
git reset $COMMIT
git commit --allow-empty --amend -am "$(git log -1 --pretty=%B) [skip ci]"
git push
else
echo "Problems syncing noir. We may need to pull the subrepo."
exit 1
Expand All @@ -109,7 +108,7 @@ jobs:
cd noir-repo
git fetch # see recent change
git checkout $BRANCH || git checkout -b $BRANCH
git merge -Xtheirs $STAGING_BRANCH
git merge -Xtheirs origin/$STAGING_BRANCH
git push origin $BRANCH
cd ..
}
Expand Down
4 changes: 2 additions & 2 deletions noir/.gitrepo
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
[subrepo]
remote = https://github.com/noir-lang/noir
branch = aztec-packages
commit = 5f5843e35052b9d3599b8ab4f7633db0a225e82f
parent = e5ca533ea4513cf3c6b7e3eb057083838b861a6b
commit = 6ff518af281afe601edb8574d425b07d9d2f9c5d
parent = 2082fedfb03d4882a269881f51c5337263bc539b
method = merge
cmdver = 0.4.6
Loading