idris-1.2.0: test/st005/run
#!/usr/bin/env bash
${IDRIS:-idris} $@ -p contrib test005.idr -o test005
echo "# test005:"
./test005
cat writeTestFile
rm -f test005 writeTestFile *.ibc
#!/usr/bin/env bash
${IDRIS:-idris} $@ -p contrib test005.idr -o test005
echo "# test005:"
./test005
cat writeTestFile
rm -f test005 writeTestFile *.ibc