From 1d7378778a70ce58e264f62820ad4d07a8609954 Mon Sep 17 00:00:00 2001
From: Niklas Larsson <niklas@mm.st>
Date: Wed, 8 Jul 2020 22:33:37 +0200
Subject: [PATCH] Fix bootstrap

This was broken in #425, because Idris2-boot hasn't implemented the
fix for #116
---
 src/Idris/Package.idr | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr
index b8289b995..49772a7dd 100644
--- a/src/Idris/Package.idr
+++ b/src/Idris/Package.idr
@@ -460,11 +460,12 @@ runRepl : {auto c : Ref Ctxt Defs} ->
 runRepl fname = do
   u <- newRef UST initUState
   m <- newRef MD initMetadata
-  case fname of
-    Nothing => pure ()
-    Just fn => do
-      errs <- loadMainFile fn
-      displayErrors errs
+  the (Core ()) $
+      case fname of
+          Nothing => pure ()
+          Just fn => do
+            errs <- loadMainFile fn
+            displayErrors errs
   repl {u} {s}