Zulip Chat Archive
Stream: general
Topic: set.mono_image
Kenny Lau (Feb 22 2019 at 14:40):
Should be changed to set.image_mono?
Patrick Massot (Feb 22 2019 at 14:54):
grep -R "lemma [^ ]*_mono" vs grep -R "lemma mono_[^ ]*" suggests you are right
Last updated: Dec 20 2023 at 11:08 UTC