idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

[ test ] Fix timing issue in interactive045 test

Browse Source
This commit is contained in:
Steve Dunham 2022-09-05 19:36:29 -07:00 committed by G. Allais
parent ece1198074
commit 9646b31f2b
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
tests/idris2/interactive045/run
View File

@ -2,6 +2,7 @@ rm -rf build
rm -f Issue1742Gen.idr
cp Issue1742.idr Issue1742Gen.idr
sleep 1
$1 --no-color --console-width 0 --no-banner Issue1742Gen.idr < input