Skip to content

Update dependency: deps/stable-mir-json_release#998

Open
rv-jenkins wants to merge 7 commits intomasterfrom
_update-deps/runtimeverification/stable-mir-json
Open

Update dependency: deps/stable-mir-json_release#998
rv-jenkins wants to merge 7 commits intomasterfrom
_update-deps/runtimeverification/stable-mir-json

Conversation

@rv-jenkins
Copy link
Copy Markdown
Contributor

No description provided.

@dkcumming
Copy link
Copy Markdown
Collaborator

dkcumming commented Mar 29, 2026

@cds-amal 142 seems to be adding some regressions for times.

20min timeout failures (this PR): 1, 2, 3 in progress

Other PRs: 10.5min, 7.5min.

We on'y recently added the timeout, so I don't actually know if this is flakiness with the runners. It really could be the case that 20min has been seen before and I just need to increase the timeout.

No request btw. I am just informing you, going to look at what I can to see if this is expected but I don't think it changes anything from your end.

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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants