mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-30 07:02:24 +03:00
9bd32c4a3d
This prints lots of warnings since incremental compilation is not available, so turn that off when running on windows for now.
10 lines
323 B
Plaintext
10 lines
323 B
Plaintext
if [ "$OS" = "windows" ]; then
|
|
# incremental builds don't work on windows so we get lots of warnings,
|
|
# but we still need the test output to be correct
|
|
$1 --no-banner --no-color --console-width 0 Main.idr < input
|
|
else
|
|
$1 --no-banner --no-color --console-width 0 Main.idr --inc chez < input
|
|
fi
|
|
|
|
rm -rf build
|