From ab6de0edcda70a5cc4d3f17ff2368438e1b5fc17 Mon Sep 17 00:00:00 2001 From: Philip Rasmussen Date: Wed, 23 Apr 2014 10:01:56 +0200 Subject: [PATCH] Changed test implementation --- test/idrisdoc007/do_not_delete_doc/dummy.txt | 1 - test/idrisdoc007/run | 3 ++- 2 files changed, 2 insertions(+), 2 deletions(-) delete mode 100644 test/idrisdoc007/do_not_delete_doc/dummy.txt diff --git a/test/idrisdoc007/do_not_delete_doc/dummy.txt b/test/idrisdoc007/do_not_delete_doc/dummy.txt deleted file mode 100644 index 10a17d4dd..000000000 --- a/test/idrisdoc007/do_not_delete_doc/dummy.txt +++ /dev/null @@ -1 +0,0 @@ -Only here to ensure that the parent directory exists. \ No newline at end of file diff --git a/test/idrisdoc007/run b/test/idrisdoc007/run index b380cf6fb..805df78e7 100755 --- a/test/idrisdoc007/run +++ b/test/idrisdoc007/run @@ -1,5 +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: @@ -7,4 +8,4 @@ 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 -f *.ibc lines \ No newline at end of file +rm -rf do_not_delete_doc *.ibc lines \ No newline at end of file