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

Correct error018 test

Browse Source 
I expect I got my local versions inconsistent while working on this...
This commit is contained in:
Edwin Brady 2021-07-20 17:02:39 +01:00 committed by Edwin Brady
parent edefd543f7
commit e633a9fa6e
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tests/idris2/error018/expected
View File

@ -30,7 +30,7 @@ Issue1031-3:4:6--4:7
1/1: Building Issue1031-4 (Issue1031-4.idr)
Error: While processing left hand side of nice. Unsolved holes:
Main.{dotTm:404} introduced at:
Main.{dotTm:373} introduced at:
Issue1031-4:4:6--4:10
1 | %default total
2 |