indentation with `classical`

Stream: general

[Sebastien Gouezel]

What is the current indentation rule with the classical tactic? Should everything be indented one step more after it (which I find quite ugly) or should we just treat it as a usual tactic, not creating more indentation?

[Kyle Miller]

I like not indenting, unless for some reason you do want to run some later tactics outside classical.

[Eric Wieser]

Mathport chooses not to indent

[Eric Wieser]

(but earlier versions didn't)