chore: disable format on save by default for lean files - #798

chore: disable format on save by default for lean files#798

mhuisi merged 1 commit into

masterleanprover/vscode-lean4:masterfrom

push-lkpvkxktysvuleanprover/vscode-lean4:push-lkpvkxktysvuCopy head branch name to clipboard