@@ -1,5 +1,6 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2# Tests that documentation only is written when safe
2# Tests that documentation only is written when safe
3+mkdir do_not_delete_doc
3idris --mkdoc package.ipkg > lines
4idris --mkdoc package.ipkg > lines
4echo Expects exit status 1: $?
5echo Expects exit status 1: $?
5echo Expects 2 lines of output:
6echo Expects 2 lines of output:
@@ -7,4 +8,4 @@ wc -l lines
7echo Expects the first line to be type checking:
8echo Expects the first line to be type checking:
8grep "Type checking \\./A\\.idr" lines
9grep "Type checking \\./A\\.idr" lines
9echo Cannot check the second line as it contains a host-dependent string.
10echo Cannot check the second line as it contains a host-dependent string.
10−rm -f *.ibc lines
11+rm -rf do_not_delete_doc *.ibc lines