
  0 | ||| Re-exports Idris.Driver with some private declarations.
  1 | |||
  2 | ||| `Idris.Driver` private items are visible here because of the common module
  3 | ||| prefix.
  4 | |||
  5 | ||| Last updated with Idris2 commit 80fd5e4d754888e02a734b05011a98ee4334fd20.
  6 | module Idris.Driver.Extra
  7 | 
  8 | import public Idris.Driver
  9 | 
 10 | import Core.Context
 11 | import Data.List1
 12 | import Idris.Driver as D
 13 | import Idris.REPL
 14 | 
 15 | export
 16 | updateEnv : {auto c : Ref Ctxt Defs} ->
 17 |             {auto o : Ref ROpts REPLOpts} ->
 18 |             Core ()
 19 | updateEnv = D.updateEnv
 20 | 
 21 | export
 22 | splitPaths : String -> List1 String
 23 | splitPaths = D.splitPaths
 24 |