Zulip Chat Archive

Stream: lean4

Topic: ctrl-/ "toggle comment" broken in vscode-lean4 0.0.32

Mario Carneiro (Jul 16 2021 at 20:58):

Using ctrl-/ or the Toggle Line Comment option from the menu fails in the latest version of the lean4 vscode extension, released 2 days ago. Downgrading to 0.0.31 appears to fix the issue.

Mario Carneiro (Jul 16 2021 at 21:06):

cc: @Wojciech Nawrocki since the main thing in 0.0.32 is the large PR vscode-lean4#30

Wojciech Nawrocki (Jul 16 2021 at 21:06):

Thanks, I'll look into it.

Last updated: Dec 20 2023 at 11:08 UTC