[Merged by Bors] - chore: move Data/Real/GoldenRatio and RingTheory/Real/Irrational to NumberTheory/Real #239194
grunwegbuild_fork.yml
on: pull_request_target
Build (fork)
11m 58s
Lint style (fork)
1m 51s
Post-CI job (fork)
8s
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
import-graph
|
247 KB |
sha256:89f7360566913ebfd9a16cc94398e46fb20bc0bd9e1553bd8959de4604122bcc
|
|
|
mathlib4_artifact
|
1.61 GB |
sha256:6e9e37b7268076d8d2bf077d3d6c5378b8a768e4c32ef63b6892000778a36f37
|
|