Zulip Chat Archive
Stream: triage
Topic: PR !4#15937: test: add autolabelling of PRs in Lean
Random Issue Bot (Oct 11 2024 at 14:10):
Today I chose PR 15937 for discussion!
test: add autolabelling of PRs in Lean
Created by @damiano (@adomani) on 2024-08-18
Labels: WIP, t-meta
Is this PR still relevant? Any recent updates? Anyone making progress?
Michael Rothgang (Oct 11 2024 at 15:35):
This PR can be closed, right?
Last updated: May 02 2025 at 03:31 UTC