Zulip Chat Archive

Stream: new members

Topic: Error message in VS Code


view this post on Zulip Ali Sever (Aug 02 2018 at 11:38):

In tactic mode if there is an error, it lists the current tactic state with n goals, and then the error, followed by the tactic state again. Is there a setting to make it show the error first? Currently I have to scroll down to see the error every time I change something.

view this post on Zulip Kevin Buzzard (Aug 02 2018 at 11:40):

Some might say that if you have to scroll down then you have too much in your tactic state :-)


Last updated: May 10 2021 at 00:31 UTC