lean4-htt/.github
Joachim Breitner f9f278266e
chore: ci to set “changes-stage0” label (#3979)
Expands on #3971 to do something useful even before the PR enters the
queue:

If stage0 changes are detected in the PR, set the changes-stage0 label
(which
has a tooltip to explain what this entail), and also remove the label if
it no
longer applies.
2024-04-24 07:08:34 +00:00
..
ISSUE_TEMPLATE chore: Issue template: Suggest #eval Lean.versionString (#2884) 2023-11-16 18:40:55 +01:00
workflows chore: ci to set “changes-stage0” label (#3979) 2024-04-24 07:08:34 +00:00
PULL_REQUEST_TEMPLATE.md chore: refine PR template (#3074) 2023-12-18 13:47:04 +00:00