From 00841033d80b666b2fb05b7bd9577eeed41edd29 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 31 Dec 2020 11:08:47 +0100
Subject: [PATCH] chore: Hover.lean ~> LanguageFeatures.lean

---
 src/Lean/Data/Lsp.lean                                  | 2 +-
 src/Lean/Data/Lsp/{Hover.lean => LanguageFeatures.lean} | 2 --
 2 files changed, 1 insertion(+), 3 deletions(-)
 rename src/Lean/Data/Lsp/{Hover.lean => LanguageFeatures.lean} (94%)

diff --git a/src/Lean/Data/Lsp.lean b/src/Lean/Data/Lsp.lean
index 23128e8390..1d50d14bd4 100644
--- a/src/Lean/Data/Lsp.lean
+++ b/src/Lean/Data/Lsp.lean
@@ -9,8 +9,8 @@ import Lean.Data.Lsp.Capabilities
 import Lean.Data.Lsp.Communication
 import Lean.Data.Lsp.Diagnostics
 import Lean.Data.Lsp.Extra
-import Lean.Data.Lsp.Hover
 import Lean.Data.Lsp.InitShutdown
+import Lean.Data.Lsp.LanguageFeatures
 import Lean.Data.Lsp.TextSync
 import Lean.Data.Lsp.Utf16
 import Lean.Data.Lsp.Workspace
diff --git a/src/Lean/Data/Lsp/Hover.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean
similarity index 94%
rename from src/Lean/Data/Lsp/Hover.lean
rename to src/Lean/Data/Lsp/LanguageFeatures.lean
index 68d2500e4a..0d58cf0b8a 100644
--- a/src/Lean/Data/Lsp/Hover.lean
+++ b/src/Lean/Data/Lsp/LanguageFeatures.lean
@@ -7,8 +7,6 @@ Authors: Wojciech Nawrocki
 import Lean.Data.Json
 import Lean.Data.Lsp.Basic
 
-/-! Handling of mouse hover requests. -/
-
 namespace Lean
 namespace Lsp