Skip to content

[Merged by Bors] - chore: yet again, some removed variables #706

[Merged by Bors] - chore: yet again, some removed variables

[Merged by Bors] - chore: yet again, some removed variables #706

Triggered via pull request October 9, 2024 12:02
Status Success
Total duration 1m 12s
Artifacts

add_label_from_diff.yaml

on: pull_request
Add topic label
1m 4s
Add topic label
Fit to window
Zoom out
Zoom in

Annotations

2 notices
Add topic label
Applicable labels: #[t-algebra, t-category-theory, t-combinatorics, t-data, t-logic, t-order]
Add topic label
not adding multiple labels: #[t-algebra, t-category-theory, t-combinatorics, t-data, t-logic, t-order]