Skip to content

chore: change pp_nodot adaptation note links to lean4 issue #1910 t… #12162

chore: change pp_nodot adaptation note links to lean4 issue #1910 t…

chore: change pp_nodot adaptation note links to lean4 issue #1910 t… #12162

Triggered via push November 23, 2024 06:30
Status Success
Total duration 25m 35s
Artifacts 1

bors.yml

on: push
Cancel Previous Runs (CI)
4s
Cancel Previous Runs (CI)
Post-CI job
9s
Post-CI job
Fit to window
Zoom out
Zoom in

Artifacts

Produced during runtime
Name Size
import-graph
178 KB