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: May 02 2025 at 03:31 UTC