From eabbc5bb68cbeeeb1ae853f352d5d46948499fa1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 15 Jan 2017 23:18:44 +0100
Subject: [PATCH] chore(library/module_mgr): comment unreachable_code assertion

@gebner, could you please take a look a check whether there is a better fix.
---
 src/library/module_mgr.cpp | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp
index ce6c5b33c5..8dfd1e29ee 100644
--- a/src/library/module_mgr.cpp
+++ b/src/library/module_mgr.cpp
@@ -65,7 +65,14 @@ static module_loader mk_loader(module_id const & cur_mod, std::vector<module_inf
                 }
             }
         } catch (std::out_of_range) {
-            lean_unreachable();
+            /* The following line of code is reachable.
+               Repro: create a file containing an "open" comment block.
+               Example:
+
+                 /-
+                   def x := 10
+            */
+            // lean_unreachable();
         }
         throw exception(sstream() << "could not resolve import: " << import.m_name);
     };