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

Merge compatible to develop #11205

Merged
merged 6 commits into from
Jun 7, 2022

Conversation

georgeee
Copy link
Member

@georgeee georgeee commented Jun 7, 2022

Merge compatible to develop.

When merging there was a conflict of src/lib/zexe_backend/zexe_backend_common/dune being absent in develop and present compatible, which was simply ignored.

@georgeee georgeee requested review from a team, bkase, psteckler, imeckler and mrmr1993 as code owners June 7, 2022 12:39
@yorickvP
Copy link
Collaborator

yorickvP commented Jun 7, 2022

Hm. That'd be my fault.

@georgeee georgeee added the ci-build-me Add this label to trigger a circle+buildkite build for this branch label Jun 7, 2022
@yorickvP
Copy link
Collaborator

yorickvP commented Jun 7, 2022

I merged #11174 and #11173 in the wrong order, I'm not sure if the "merges cleanly" check is correct, because I can merge this just fine at home. But develop -> compatible is broken indeed.

@mrmr1993 mrmr1993 merged commit 7028850 into develop Jun 7, 2022
@mrmr1993 mrmr1993 deleted the georgeee/merge-compatible-to-develop-2022-06-07 branch June 7, 2022 14:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ci-build-me Add this label to trigger a circle+buildkite build for this branch
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants