Skip to content

chore(Algebra/Order/Floor): Split off round section (#20831) #13136

chore(Algebra/Order/Floor): Split off round section (#20831)

chore(Algebra/Order/Floor): Split off round section (#20831) #13136

Triggered via push January 18, 2025 20:29
Status Failure
Total duration 25m 13s
Artifacts 1

bors.yml

on: push
Fit to window
Zoom out
Zoom in

Annotations

1 error and 1 warning
Build
The process '/usr/bin/env' failed with exit code 1
Build: Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean#L8
unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)

Artifacts

Produced during runtime
Name Size
import-graph
190 KB