mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-29 15:52:29 +03:00
4f21234c9e
how to take care of input termination properly? currently we add the message 'Alas the file is done' in the expected outcome but that's ugly |
||
---|---|---|
.. | ||
expected | ||
input | ||
LocType.idr | ||
run |