idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

Fix bootstrap

Browse Source 
This was broken in #425, because Idris2-boot hasn't implemented the
fix for #116
This commit is contained in:
Niklas Larsson 2020-07-08 22:33:37 +02:00
parent b955d2e50c
commit 1d7378778a
1 changed files with 6 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/Idris/Package.idr
View File

@ -460,11 +460,12 @@ runRepl : {auto c : Ref Ctxt Defs} ->
runRepl fname = do runRepl fname = do
u <- newRef UST initUState u <- newRef UST initUState
m <- newRef MD initMetadata m <- newRef MD initMetadata
case fname of the (Core ()) $
Nothing => pure () case fname of
Just fn => do Nothing => pure ()
errs <- loadMainFile fn Just fn => do
displayErrors errs errs <- loadMainFile fn
displayErrors errs
repl {u} {s} repl {u} {s}