From 71524d9c9095459a05a900aacefd481d45a314a7 Mon Sep 17 00:00:00 2001 From: zoomiti Date: Sun, 18 Sep 2022 18:53:48 -0400 Subject: [PATCH] Removes Lean LSP from nvim --- .config/nvim/init.vim | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.config/nvim/init.vim b/.config/nvim/init.vim index fdf9e95..cc2f806 100644 --- a/.config/nvim/init.vim +++ b/.config/nvim/init.vim @@ -72,7 +72,7 @@ Plug 'kyazdani42/nvim-web-devicons' Plug 'mfussenegger/nvim-dap' " Lean requires nvim -Plug 'Julian/lean.nvim' +" Plug 'Julian/lean.nvim' Plug 'nvim-lua/plenary.nvim' Plug 'andrewradev/switch.vim' " For Lean switch support Plug 'norcalli/nvim-colorizer.lua' " For colorizing @@ -430,6 +430,7 @@ if has("nvim") require('rust-tools').setup({ server = {capabilities = capabilities, on_attach = on_attach } }) + --[[ require('lean').setup{ --{{{ -- Enable the Lean language server(s)? -- @@ -491,6 +492,7 @@ if has("nvim") priority = 10, }, } -- }}} + --]] EOF endif