idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-29 14:44:03 +03:00
Code Issues Projects Releases Wiki Activity

Add missing import

Browse Source 
This wouldn't have got caught since the merge that caused the problem
was checked before I pushed the patch that made import work right! So
hopefully this'll sort it.
This commit is contained in:
Edwin Brady 2020-05-27 21:44:37 +01:00
parent 6b8324db3b
commit 1c889ec99e
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/Utils/Path.idr
View File

@ -2,6 +2,7 @@ module Utils.Path
import Data.List
import Data.Maybe
import Data.Nat
import Data.Strings
import Data.String.Extra