Skip to content

Merge remote-tracking branch 'upstream/master' into bump/v4.27.0 #5611

Merge remote-tracking branch 'upstream/master' into bump/v4.27.0

Merge remote-tracking branch 'upstream/master' into bump/v4.27.0 #5611

Triggered via push December 11, 2025 03:48
Status Success
Total duration 1h 4m 21s
Artifacts 2

build.yml

on: push
Fit to window
Zoom out
Zoom in

Annotations

1 error
Build
Process completed with exit code 3.

Artifacts

Produced during runtime
Name Size Digest
import-graph
261 KB
sha256:fd159b193038a9348e6fcaccb069b74fe01d9245e3b8a975a5777a263da13101
mathlib4_artifact
2.01 GB
sha256:5f04ecc9c163e7b5999c935aba9882a96b03bae0237e80f1da4a1a5050124aba