Zulip Chat Archive
Stream: triage
Topic: issue #10954: Add an @[intuit] attribute or similar
Random Issue Bot (Feb 10 2022 at 14:16):
Today I chose issue 10954 for discussion!
Add an @[intuit] attribute or similar
Created by @Eric Wieser (@eric-wieser) on 2021-12-21
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jun 27 2022 at 14:22):
Today I chose issue 10954 for discussion!
Add an @[intuit] attribute or similar
Created by @Eric Wieser (@eric-wieser) on 2021-12-21
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Sep 06 2022 at 14:18):
Today I chose issue 10954 for discussion!
Add an @[intuit] attribute or similar
Created by @Eric Wieser (@eric-wieser) on 2021-12-21
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Oct 29 2022 at 14:19):
Today I chose issue 10954 for discussion!
Add an @[intuit] attribute or similar
Created by @Eric Wieser (@eric-wieser) on 2021-12-21
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Oct 29 2022 at 14:37):
Can we start closing such issues with comments such as "maybe mathlib4"? (if indeed that is what the community things about this and perhaps other issues)
Yaël Dillies (Oct 29 2022 at 14:38):
I was actually thinking of working on this.
Eric Wieser (Oct 29 2022 at 14:41):
I think this one is a pretty trivial y'all of copying code from zulip into a PR
Random Issue Bot (May 29 2023 at 14:07):
Today I chose issue 10954 for discussion!
Add an @[intuit] attribute or similar
Created by @Eric Wieser (@eric-wieser) on 2021-12-21
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Aug 11 2023 at 14:08):
Today I chose issue 10954 for discussion!
Add an @[intuit] attribute or similar
Created by @Eric Wieser (@eric-wieser) on 2021-12-21
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC