Skip to content

Commit

Permalink
[ re #3066 ] Make the rest of tests to use the same form as the others
Browse files Browse the repository at this point in the history
  • Loading branch information
buzden committed Oct 3, 2023
1 parent f303d9e commit 14b6cb4
Show file tree
Hide file tree
Showing 6 changed files with 17 additions and 17 deletions.
7 changes: 4 additions & 3 deletions tests/idris2/basic/basic071/run
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
rm -rf build
$1 --no-color --console-width 0 --no-banner --check B.idr
. ../../../testutils.sh

check B.idr

# Set very close time for A and B TTC files
touch A.idr
Expand All @@ -13,4 +14,4 @@ sync build/ttc/*/B.tt*

echo "-- this should be the last line of output --"

$1 --no-color --console-width 0 --no-banner --check B.idr
check B.idr
6 changes: 3 additions & 3 deletions tests/idris2/basic/case001/run
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
rm -rf build
. ../../../testutils.sh

$1 --no-color --console-width 0 --no-banner --codegen chez InlineCase.idr -o inline-case
grep "define InlineCase-product" build/exec/inline-case_app/inline-case.ss
idris2 --codegen chez InlineCase.idr -o inline-case
grep "define InlineCase-product" build/exec/inline-case_app/inline-case.ss
4 changes: 2 additions & 2 deletions tests/idris2/basic/case002/run
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
rm -rf build
. ../../../testutils.sh

$1 --no-color --console-width 0 --no-banner --check WhereData.idr
check WhereData.idr
4 changes: 2 additions & 2 deletions tests/idris2/basic/literals001/run
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
rm -rf build
. ../../../testutils.sh

$1 --no-color --console-width 0 --no-banner -c Test.idr
check Test.idr
4 changes: 2 additions & 2 deletions tests/idris2/literate/literate018/run
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
rm -rf build
. ../../../testutils.sh

$1 --no-color --console-width 0 --no-banner --check Test.lidr.md
check Test.lidr.md
9 changes: 4 additions & 5 deletions tests/idris2/total/total021/run
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
rm -rf build

$1 --no-color --console-width 0 --no-banner --check Issue-3030.idr
$1 --no-color --console-width 0 --no-banner --check Issue-3030b.idr
$1 --no-color --console-width 0 --no-banner --check Issue-524.idr
. ../../../testutils.sh

check Issue-3030.idr
check Issue-3030b.idr
check Issue-524.idr

0 comments on commit 14b6cb4

Please sign in to comment.