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