Zulip Chat Archive
Stream: general
Topic: hole command in tactic mode
Johan Commelin (Nov 20 2019 at 10:22):
Do hole commands work in tactic mode? I can see the list of hole commands, but if I select one, nothing noticeable happens.
Last updated: Dec 20 2023 at 11:08 UTC