mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 14:09:30 +03:00
Made test resistant to differences among command implementations
This commit is contained in:
parent
ab6de0edcd
commit
e202cfd65b
@ -1,6 +1 @@
|
|||||||
Expects exit status 1: 1
|
Exit status (expects 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.
|
|
||||||
|
@ -1,11 +1,6 @@
|
|||||||
#!/usr/bin/env bash
|
#!/usr/bin/env bash
|
||||||
# Tests that documentation only is written when safe
|
# Tests that documentation only is written when safe
|
||||||
mkdir do_not_delete_doc
|
mkdir do_not_delete_doc
|
||||||
idris --mkdoc package.ipkg > lines
|
idris --mkdoc package.ipkg > nowhere
|
||||||
echo Expects exit status 1: $?
|
echo Exit status \(expects 1\): $?
|
||||||
echo Expects 2 lines of output:
|
rm -rf do_not_delete_doc *.ibc nowhere
|
||||||
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
|
|
Loading…
Reference in New Issue
Block a user