search

imandra-ai / imandra-vscode

VSCode extension for developing imandra
Other
2 stars 0 forks source link

Fix comment pairs #16

Closed actionshrimp closed 5 years ago

actionshrimp commented 5 years ago

This seems to be a vscode issue with autoClosingPairs: https://github.com/Microsoft/vscode/issues/72177

Removing the comment markers from there makes it less annoying - isn't perfect but seems preferable.