PR #5591: feat(geometry/manifold/instances): sphere is a ...

Stream: triage

[Random Issue Bot]

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]

Hmm, the bot is not very smart. The last dependency for this PR was merged this morning.

[Rob Lewis]

The bot isn't smart at all, don't put too much thought into its prods!

[Bryan Gin-ge Chen]

Would it help if we changed this line to use i.updated_at?

[Rob Lewis]

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]

leanprover-community/azure-scripts#8 uses update time and delta of 7 days