Skip to content
lint and suggest

[Merged by Bors] - feat: introduce the missing notation for AddHom #69300

Sign in to view logs

[Merged by Bors] - feat: introduce the missing notation for AddHom

[Merged by Bors] - feat: introduce the missing notation for AddHom #69300

Triggered via pull request November 22, 2024 23:19
@PieterCuijpersPieterCuijpers
synchronize #19387
PieterCuijpers_AddHom_Notation
Status Success
Total duration 2m 34s
Artifacts –

lint_and_suggest_pr.yml

on: pull_request
Lint style
1m 36s
Lint style
Check all files imported
35s
Check all files imported
Fit to window
Zoom out
Zoom in