mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
[ re #2884 ] Move existing test to an appropriate category
This commit is contained in:
parent
46483fd120
commit
0c40a76c2c
3
tests/base/sortedmap_001/run
Normal file
3
tests/base/sortedmap_001/run
Normal file
@ -0,0 +1,3 @@
|
||||
. ../../testutils.sh
|
||||
|
||||
run SortedMapTest.idr
|
@ -1,3 +0,0 @@
|
||||
. ../../testutils.sh
|
||||
|
||||
run -p contrib SortedMapTest.idr
|
Loading…
Reference in New Issue
Block a user