Skip to content

Default to panic = "abort" #567

Default to panic = "abort"

Default to panic = "abort" #567

Triggered via pull request October 31, 2024 01:37
Status Failure
Total duration 46m 54s
Artifacts

push.yaml

on: pull_request
Fit to window
Zoom out
Zoom in

Annotations

2 errors and 6 warnings
Run other tests
The hosted runner encountered an error while running your job. (Error Type: Disconnect).
Run other tests
The hosted runner: GitHub Actions 55 lost communication with the server. Anything in your workflow that terminates the runner process, starves it for CPU/Memory, or blocks its network access can cause this error.
Check source
No push credentials found. Ignoring the 'useDaemon' option.
Build docs
No push credentials found. Ignoring the 'useDaemon' option.
Check dependencies
No push credentials found. Ignoring the 'useDaemon' option.
Check Kani proofs
No push credentials found. Ignoring the 'useDaemon' option.
Run other tests
Received request to deprovision: The request was cancelled by the remote provider.
Run other tests
No push credentials found. Ignoring the 'useDaemon' option.