Added test case directive002
commitd4d4ba63104f57e4fdd0a560890c970a4fc069f7
authorColin Adams <colinpauladams@gmail.com>
dateFri 6 May 2016, 18:29 (10 years ago)
parent41e3c52
idris.cabal+3
@@ -414,6 +414,9 @@ Extra-source-files:
414414 test/directives001/*.idr
415415 test/directives001/run
416416 test/directives001/expected
417+ test/directives002/*.idr
418+ test/directives002/run
419+ test/directives002/expected
417420
418421 test/delab001/*.idr
419422 test/delab001/run
test/directives002/directives002.idrnew file+14
@@ -0,0 +1,14 @@
1+module directives002
2+
3+%access export
4+%default covering
5+
6+loop : ()
7+loop = loop
8+
9+namespace Main
10+ total
11+ main : IO ()
12+ main = do
13+ pure loop
14+ putStrLn $ "Hello World"
test/directives002/expectednew file+2
@@ -0,0 +1,2 @@
1+directives002.idr:12:3:
2+directives002.Main.main is possibly not total due to: directives002.loop
test/directives002/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ directives002.idr --check --nocolour
3+
4+rm -f directives002 *.ibc