Skip to content

github: rename jj-docs-bot to jj-docs[bot] #6888

github: rename jj-docs-bot to jj-docs[bot]

github: rename jj-docs-bot to jj-docs[bot] #6888

Triggered via push September 16, 2023 02:31
Status Success
Total duration 11m 21s
Artifacts
This run and associated checks have been archived and are scheduled for deletion. Learn more about checks retention

build.yml

on: push
Check protos
53s
Check protos
Check formatting
16s
Check formatting
Check that MkDocs can build the docs
31s
Check that MkDocs can build the docs
Clippy check
2m 53s
Clippy check
Matrix: build
Matrix: cargo-deny
Fit to window
Zoom out
Zoom in