mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-17 10:58:20 +03:00
1b36dd99b1
Back ends can still shortcut these and use their own primitives, but doing things this way gives consistent behaviour between the simple IO primitives and file IO, and allow us to use stdin/stdout consistently (e.g. to flush stdout). This also fixes the behaviour of 'replWith' to be consistent with the Idris 1 version.
4 lines
46 B
Plaintext
Executable File
4 lines
46 B
Plaintext
Executable File
$1 --no-banner Main.idr < input
|
|
|
|
rm -rf build
|