fix: remove backtick name highlighting#692

mhuisi merged 1 commit intoleanprover:masterleanprover/vscode-lean4:masterfrom

mhuisi:push-ltmtwotpwrrqmhuisi/vscode-lean4:push-ltmtwotpwrrqCopy head branch name to clipboard