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 functionality to filter out tests #9

Open
wants to merge 14 commits into
base: Latest
Choose a base branch
from
Prev Previous commit
Next Next commit
nightly build failed (dafny-lang#2161)
  • Loading branch information
MikaelMayer committed Jul 1, 2022
commit 52405d17ba6e0c7d8df0fd4affa75c3e82e69e77
11 changes: 11 additions & 0 deletions .github/CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -26,3 +26,14 @@ All other pull requests and issues can be submitted here.
## Code of Conduct

See [`CODE_OF_CONDUCT.md`](./CODE_OF_CONDUCT.md).

## FAQ

### What to do if the nightly build failed but because of a "download failure"?

If the test in a PR named `Build and Test / check-deep-tests / check-deep-tests` failed, clicking on its "details" reveals a view (view 1) in which you can see a failed run with the failure being something like "Error: Last run of deep-tests.yml did not succeed (some URL in parentheses).

Clicking on this URL will reveal the deep tests that were run (view 2). If one of this test is just a "download failure", then one simply needs to re-run it (button on the top right).
Once it succeeds, one has to go back to (view 1) and re-run the failed jobs, so that it will retrieve the latest successful deep tests.

After doing these steps once, for other PRs, one only needs to re-run deep checks in (view 1)