config-schema: expand options for ui.editor, ui.diff.tool, and ui.pager
#19282
Triggered via pull request
February 11, 2025 00:41
Status
Success
Total duration
14m 25s
Artifacts
–
build.yml
on: pull_request
Build without Git support
1m 15s
Check protos
33s
Check formatting
19s
Codespell
8s
Run doctests
2m 33s
Check that MkDocs can build the docs
10s
Check that MkDocs can build the docs with latest Python and uv
10s
Clippy check
3m 2s
Matrix: build
Matrix: cargo-deny