git.iko.soy/Idris-dev
on master help sign in
Add a test for compiler filename warnings
c629b60David Raymond Christiansen
test/interactive005/expected+1
compare with master
unifiedsplit
@@ -31,3 +31,4 @@ main : IO ()
31 This is a docstring
31 This is a docstring
32
32
33Nat2 : Type
33Nat2 : Type
34+Invalid filename for compiler output "Test.idr"
test/interactive005/input+2
@@ -19,3 +19,5 @@ the Nat (1 + 2)
19:doc main
19:doc main
20:let data Nat2 = Zero | Succ Nat2
20:let data Nat2 = Zero | Succ Nat2
21:t Nat2
21:t Nat2
22+:compile Test.idr
23+:compile a.out
test/interactive005/run+1
@@ -3,3 +3,4 @@ idris --quiet interactive005.idr < input
3rm -f *.ibc
3rm -f *.ibc
4rm -f hello.bytecode
4rm -f hello.bytecode
5rm -f hello
5rm -f hello
6+rm -f a.out