Random Issue Bot (Jan 28 2021 at 14:24):
Today I chose PR 5591 for discussion!
feat(geometry/manifold/instances): sphere is a topological manifold
Created by @None (@hrmacbeth) on 2021-01-03
Labels: awaiting-author, merge-conflict
Is this PR still relevant? Any recent updates? Anyone making progress?
Heather Macbeth (Jan 28 2021 at 16:10):
Hmm, the bot is not very smart. The last dependency for this PR was merged this morning.
Rob Lewis (Jan 28 2021 at 16:36):
The bot isn't smart at all, don't put too much thought into its prods!
Bryan Gin-ge Chen (Jan 28 2021 at 16:56):
Would it help if we changed this line to use
Rob Lewis (Jan 28 2021 at 17:00):
Sure, depending on what we want the behavior to be. If it goes off update time instead of post time maybe it's worth lowering the time delta a bit.
Bryan Gin-ge Chen (Jan 28 2021 at 17:08):
leanprover-community/azure-scripts#8 uses update time and delta of 7 days
Last updated: May 09 2021 at 15:11 UTC