Skip to content

Fix problems with error on the first command of a file. #769

Fix problems with error on the first command of a file.

Fix problems with error on the first command of a file. #769

Re-run triggered March 22, 2025 08:49
Status Success
Total duration 4m 38s
Artifacts

test.yml

on: pull_request
Matrix: build
Matrix: check-doc-magic
Matrix: compile-tests
Matrix: simple-tests
Matrix: test-indent
Matrix: test-qrhl
Matrix: test
Fit to window
Zoom out
Zoom in

Annotations

1 warning
compile-tests (coq-8.13.2-emacs-27.2)
Failed to remove 'http.https://github.com/.extraheader' from the git config