mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-11 03:34:13 +03:00
Remove reliance on interactive output from test ffi004
This commit is contained in:
parent
835981d84e
commit
a27e6cba4f
@ -281,7 +281,6 @@ Extra-source-files:
|
||||
test/ffi003/input
|
||||
test/ffi004/run
|
||||
test/ffi004/*.idr
|
||||
test/ffi004/input
|
||||
test/ffi004/theType
|
||||
test/ffi004/theOtherType
|
||||
test/ffi004/expected
|
||||
|
@ -1,3 +0,0 @@
|
||||
Type checking ./test026.idr
|
||||
[?1049h[1;52r(B[m[4l[?7h[H[2J[52;1H[?1049l
[?1l>2 : Int
|
||||
[?1049h[1;52r(B[m[4l[?7h[H[2J[52;1H[?1049l
[?1l>2 : Nat
|
@ -1,2 +0,0 @@
|
||||
foo
|
||||
bar
|
@ -1,3 +1,3 @@
|
||||
#!/usr/bin/env bash
|
||||
idris --quiet --nocolour test026.idr < input
|
||||
idris --quiet --nocolour --check test026.idr
|
||||
rm -f *.ibc
|
||||
|
@ -24,3 +24,9 @@ foo = 2
|
||||
bar : T2
|
||||
bar = 2
|
||||
|
||||
testFoo : Int
|
||||
testFoo = foo
|
||||
|
||||
testBar : Nat
|
||||
testBar = bar
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user