From f4e6635f2bb34e2bb0c7d3b427232d8b525b7987 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 17 Sep 2020 13:51:02 +0200
Subject: [PATCH] chore: getMessageStringEx: show exception

---
 src/Lean/Message.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 64dd972219..b5c0fbe35f 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -172,8 +172,8 @@ instance : Inhabited Message :=
 @[export lean_message_severity] def getSeverityEx (msg : Message) : MessageSeverity := msg.severity
 @[export lean_message_string] unsafe def getMessageStringEx (msg : Message) : String :=
 match unsafeIO (msg.data.toString) with -- hack: this is going to be deleted
-| Except.ok msg => msg
-| _             => "error"
+| Except.ok msg  => msg
+| Except.error e => "error formatting message: " ++ toString e
 
 end Message