Open NotWearingPants opened 6 months ago
idtac "hello" prints hello in the output panel called "Info", but it is not discoverable since it's not opened automatically.
idtac "hello"
hello
Check 0. opens the "Notices" output panel automatically, so I think idtac should open the "Info" output panel automatically.
Check 0.
idtac
(I'm using VsCoq Legacy v0.4.0, not sure if this issue applies to VsCoq 2 since I haven't used it)
idtac "hello"printshelloin the output panel called "Info", but it is not discoverable since it's not opened automatically.Check 0.opens the "Notices" output panel automatically, so I thinkidtacshould open the "Info" output panel automatically.(I'm using VsCoq Legacy v0.4.0, not sure if this issue applies to VsCoq 2 since I haven't used it)