mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-13 15:36:41 +03:00
Added missing expected file
This commit is contained in:
parent
824d0e3ea2
commit
ae7bdd1f22
@ -570,6 +570,7 @@ Extra-source-files:
|
||||
test/pkg001/run
|
||||
test/pkg001/test.ipkg
|
||||
test/pkg001/*.idr
|
||||
test/pkg001/expected
|
||||
|
||||
test/proof001/run
|
||||
test/proof001/*.idr
|
||||
|
1
test/pkg001/expected
Normal file
1
test/pkg001/expected
Normal file
@ -0,0 +1 @@
|
||||
Type checking ./Main.idr
|
Loading…
Reference in New Issue
Block a user