From cfa02bf16a45c1da5b61c9ab74ceefe66cc134c4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 14 Oct 2020 12:05:52 -0700
Subject: [PATCH] chore: add missing `:`

---
 src/Lean/Message.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 273f763c8a..568076c01d 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -15,7 +15,7 @@ import Lean.Util.PPGoal
 
 namespace Lean
 def mkErrorStringWithPos (fileName : String) (line col : Nat) (msg : String) : String :=
-fileName ++ ":" ++ toString line ++ ":" ++ toString col ++ " " ++ toString msg
+fileName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ toString msg
 
 inductive MessageSeverity
 | information | warning | error