Skip to content

feat: Switch from "math" to "mathlib" in the lake new <project> <template> syntax #13904

feat: Switch from "math" to "mathlib" in the lake new <project> <template> syntax

feat: Switch from "math" to "mathlib" in the lake new <project> <template> syntax #13904

Triggered via pull request May 26, 2025 21:30
Status Failure
Total duration 10s
Artifacts

pr-body.yml

on: pull_request
check-pr-body
1s
check-pr-body
Fit to window
Zoom out
Zoom in

Annotations

1 error
check-pr-body
feat/fix PR must have a `changelog-*` label