From 92316dff89f5524b2dcfbf1f98dbda400d591241 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 Nov 2019 14:28:56 -0800
Subject: [PATCH] chore: remove unnecessary inline

---
 library/Init/Lean/Meta/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/Init/Lean/Meta/Basic.lean b/library/Init/Lean/Meta/Basic.lean
index 6a0fffa73b..88104bc685 100644
--- a/library/Init/Lean/Meta/Basic.lean
+++ b/library/Init/Lean/Meta/Basic.lean
@@ -135,7 +135,7 @@ do ctx ← read;
    s ← get;
    throw (f {env := s.env, mctx := s.mctx, lctx := ctx.lctx })
 
-@[inline] def throwBug {α} (b : Bug) : MetaM α :=
+def throwBug {α} (b : Bug) : MetaM α :=
 throwEx $ Exception.bug b
 
 /-- Execute `x` only in debugging mode. -/