[Agda] file for readFiniteFile

[G. Allais]

Some editors automatically insert newlines at the end of a file.
I just tested and vim & nano insert a newline character whilst
emacs does not for instance.

On 22/09/16 15:10, Nils Anders Danielsson wrote:
> On 2016-09-22 14:48, Sergei Meshveliani wrote:
>> If you set
>>             12
>>
>> into  data.txt,  the result string will have length 3.
>> I guess that the last symbol is Newline, because this is visible on the
>> screen output when running `main':
>>
>>    ...> ./TT
>>    12
>>    ...>
>>
>> instead of
>>
>>    ...> ./TT
>>    12...>
>
> If I insert "12\n" into data.txt, then the program prints a newline
> character, and if I insert "12", then it doesn't.
>