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

Removed pull request is not removed from the board #216

Closed
barmac opened this issue Nov 18, 2024 · 5 comments · Fixed by #218
Closed

Removed pull request is not removed from the board #216

barmac opened this issue Nov 18, 2024 · 5 comments · Fixed by #218
Assignees
Labels
bug Something isn't working

Comments

@barmac
Copy link
Contributor

barmac commented Nov 18, 2024

Describe the Bug

The pull request in the inbox was removed from GitHub, and the link is now dead (404):

image

Yet, the PR is stuck in our board, and you can see that in the link:

https://tasks.bpmn.io/board?c=%21Inbox&s=repo%3A%22bpmn-io%2Fdmn-js-properties-panel%22+

The pull request can be moved to another column, but then the UI reports an error. The card stays in the column though.

Screen.Recording.2024-11-18.at.16.00.17.mov

For more context, the PR was created by an AI-spam-service. So it was probably removed by some GH spam filter.

Steps to Reproduce

Create a pull request, remove it, and check the board.

Expected Behavior

Pull request is removed from the board.

Environment

https://tasks.bpmn.io

  • Host (Browser/Node version), if applicable: [e.g. MS Edge 18, Chrome 69, Node 10 LTS]
  • OS: [e.g. Windows 7]
  • Board version: [e.g. 1.0.0]
@barmac barmac added the bug Something isn't working label Nov 18, 2024
@nikku
Copy link
Owner

nikku commented Nov 18, 2024

Pull requests cannot be removed using the standard GitHub interface. So how did you do it?

screenshot LHX9RL

@nikku
Copy link
Owner

nikku commented Nov 18, 2024

Did you ask GitHub staff to delete the pull request? If so, why?

This tools operates on standard GitHub events and API, I'm afraid it cannot simply compensate for internal maintainance operations.

nikku added a commit that referenced this issue Nov 18, 2024
Pull requests cannot be deleted via API, only internally by GitHub staff.
This may lead to PR references to be "dangling".

Closes #216
nikku added a commit that referenced this issue Nov 18, 2024
Pull requests cannot be deleted via API, only internally by GitHub staff.
This may lead to PR references to be "dangling". The resolution is to
treat all open PRs that could not be fetched as "upstream deleted".

Worst case these PRs will re-appear onto the board on PR activity, or
next background sync.

Closes #216
@nikku nikku closed this as completed in cf9cfa3 Nov 18, 2024
@nikku
Copy link
Owner

nikku commented Nov 18, 2024

I shipped a fix via #218 and will test this one, if it works we're lucky, otherwise manual data maintainance is needed to fix this edge case.

@nikku
Copy link
Owner

nikku commented Nov 18, 2024

You may update to v0.63.1 and see if it solves your issue.

@nikku nikku self-assigned this Nov 18, 2024
@barmac
Copy link
Contributor Author

barmac commented Nov 19, 2024

Did you ask GitHub staff to delete the pull request? If so, why?

This tools operates on standard GitHub events and API, I'm afraid it cannot simply compensate for internal maintainance operations.

I did not! But it's not there. I assume this was removed by some anti-spam measures, but cannot tell for sure. I only got an email about the PR but the link was already dead when I clicked it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants