mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-23 20:22:34 +03:00
Shuffle some tests around
Making sure that tests which use chez are run after we've checked chez is installed
This commit is contained in:
parent
2ad1621a3e
commit
2b6000ecac
@ -81,7 +81,7 @@ idrisTests
|
||||
-- Miscellaneous regressions
|
||||
"reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
|
||||
"reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
|
||||
"reg015", "reg016", "reg017",
|
||||
"reg015", "reg016",
|
||||
-- Totality checking
|
||||
"total001", "total002", "total003", "total004", "total005",
|
||||
"total006",
|
||||
@ -98,7 +98,8 @@ chezTests : List String
|
||||
chezTests
|
||||
= ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
|
||||
"chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
|
||||
"chez013", "chez014", "chez015"]
|
||||
"chez013", "chez014", "chez015",
|
||||
"reg001"]
|
||||
|
||||
ideModeTests : List String
|
||||
ideModeTests
|
||||
|
10
tests/chez/reg001/expected
Normal file
10
tests/chez/reg001/expected
Normal file
@ -0,0 +1,10 @@
|
||||
3
|
||||
4.2
|
||||
"1.2"
|
||||
4
|
||||
1
|
||||
"2.7"
|
||||
5.9
|
||||
2
|
||||
2
|
||||
2
|
3
tests/chez/reg001/run
Executable file
3
tests/chez/reg001/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 numbers.idr -x main
|
||||
|
||||
rm -rf build
|
@ -1,10 +1 @@
|
||||
3
|
||||
4.2
|
||||
"1.2"
|
||||
4
|
||||
1
|
||||
"2.7"
|
||||
5.9
|
||||
2
|
||||
2
|
||||
2
|
||||
1/1: Building Using (Using.idr)
|
||||
|
@ -1,3 +1,3 @@
|
||||
$1 numbers.idr -x main
|
||||
$1 Using.idr --check
|
||||
|
||||
rm -rf build
|
||||
|
@ -1 +0,0 @@
|
||||
1/1: Building Using (Using.idr)
|
@ -1,3 +0,0 @@
|
||||
$1 Using.idr --check
|
||||
|
||||
rm -rf build
|
Loading…
Reference in New Issue
Block a user