From 104b51471cd115c7a3a2fa68cd31ba43f33372b4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 22 Apr 2021 20:38:57 -0700
Subject: [PATCH] chore: fix warning

---
 src/runtime/object.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index bd031e21db..1fdeacf4d4 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -59,6 +59,7 @@ extern "C" object * lean_panic_fn(object * default_val, object * msg) {
 
 extern "C" object * lean_sorry(uint8) {
     lean_internal_panic("executed 'sorry'");
+    lean_unreachable();
 }
 
 extern "C" size_t lean_object_byte_size(lean_object * o) {