diff --git a/test/idrisdoc007/expected b/test/idrisdoc007/expected index 68d6b507a..f6d166a54 100644 --- a/test/idrisdoc007/expected +++ b/test/idrisdoc007/expected @@ -1,6 +1 @@ -Expects exit status 1: 1 -Expects 2 lines of output: - 2 lines -Expects the first line to be type checking: -Type checking ./A.idr -Cannot check the second line as it contains a host-dependent string. +Exit status (expects 1): 1 diff --git a/test/idrisdoc007/run b/test/idrisdoc007/run index 805df78e7..928ea667e 100755 --- a/test/idrisdoc007/run +++ b/test/idrisdoc007/run @@ -1,11 +1,6 @@ #!/usr/bin/env bash # Tests that documentation only is written when safe mkdir do_not_delete_doc -idris --mkdoc package.ipkg > lines -echo Expects exit status 1: $? -echo Expects 2 lines of output: -wc -l lines -echo Expects the first line to be type checking: -grep "Type checking \\./A\\.idr" lines -echo Cannot check the second line as it contains a host-dependent string. -rm -rf do_not_delete_doc *.ibc lines \ No newline at end of file +idris --mkdoc package.ipkg > nowhere +echo Exit status \(expects 1\): $? +rm -rf do_not_delete_doc *.ibc nowhere \ No newline at end of file