Escaping in string templates confuses highlighting

Stream: lean4

[Daniel Weber]

The test2 string in here confuses the syntax highlighting in VSCode and live.lean-lang.org, and causes what's following it to be highlighted like it's inside a string, despite this being valid code.

def test := 1 + 1

def test2 : String := s!"\{"

#eval test2

def test3 := test + test + test

live.lean-lang.org:
image.png
vscode:
image.png

[Marc Huisinga]

Please report this as a bug in vscode-lean4.