Zulip Chat Archive
Stream: mathlib4
Topic: Loogle bug: cursor position when copying
Kenny Lau (Oct 11 2025 at 05:39):
If you copy a formatted text such as ProjectiveSpectrum and paste it to Loogle, it puts your cursor on the wrong positions:
Last updated: Dec 20 2025 at 21:32 UTC