chore: drop superfluous "server"

Co-authored-by: Gabriel Ebner <gebner@gebner.org>
leanprover · Aug 3, 2021 · 03baf88 · 03baf88
1 parent c19deef
commit 03baf88
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Widget/InteractiveDiagnostics.lean b/src/Lean/Widget/InteractiveDiagnostics.lean
@@ -105,7 +105,7 @@ def msgToDiagnostic (text : FileMap) (m : Message) : ReaderT RpcSession IO Diagn
     | MessageSeverity.information => DiagnosticSeverity.information
     | MessageSeverity.warning     => DiagnosticSeverity.warning
     | MessageSeverity.error       => DiagnosticSeverity.error
-  let source := "Lean 4 server"
+  let source := "Lean 4"
   let tt ← msgToInteractive m.data
   let ttJson ← toJson <$> rpcEncode tt
   pure {