Skip to content

Conversation

@josecorella
Copy link
Contributor

Issue #, if available:

Description of changes:

Squash/merge commit message, if applicable:

<type>(dafny/java/python/dotnet/go/rust): <description>

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

Comment on lines 52 to 65
- name: Create issue on rebase failure
if: steps.rebase.outputs.rebase_status == 'failed'
uses: actions/github-script@v6
with:
github-token: ${{ secrets.GITHUB_TOKEN }}
script: |
github.rest.issues.create({
owner: context.repo.owner,
repo: context.repo.repo,
title: 'Rebase failed for mutations branch',
body: `The automatic rebase of the \`mutations\` branch failed due to conflicts.\n\n` +
`This happened after a push to the default branch by ${context.actor}.\n\n` +
`Please resolve the conflicts manually.`
})
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Out of curiosity, do we create a new GHI for each commit that has conflicts or will it be added to an already cut GHI?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since there is no UUID or other reference in scope, it probably will create a new GHI.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

create a new one for each commit - highly overkill and will create lots of noise. We may opt for a different alert mechanism.

with:
github-token: ${{ secrets.GITHUB_TOKEN }}
script: |
github.rest.issues.create({
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Non blocking suggestions: We could also add a tag to the github issue

@texastony
Copy link
Contributor

Question: Would we need to collapse from 3 PRs/branches to just one?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants