Zulip Chat Archive
Stream: general
Topic: moogle dead
Kim Morrison (Sep 25 2025 at 04:26):
moogle is dead, right? I think it is time to clean up and remove #moogle etc, to avoid distracting users.
Kim Morrison (Sep 25 2025 at 05:31):
#leansearch (remember this also works as a command in Lean source files) is alive and well.
Kim Morrison (Sep 25 2025 at 08:20):
https://github.com/leanprover-community/LeanSearchClient/pull/24 removes the #moogle command
Last updated: Dec 20 2025 at 21:32 UTC