Don't try to compile a test that doesn't have `main`
Instead, just --check it.
commitcd8a233855d4358aba91d4b8d6bcfa0c7c6b4dea
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateTue 6 May 2014, 19:55 (12 years ago)
parent0cdef7f
test/totality001/run+3−3
@@ -1,6 +1,6 @@
11#!/usr/bin/env bash
2−idris $@ test010.idr -o test010
3−idris $@ test010a.idr -o test010
4−idris $@ test010b.idr -o test010
2+idris $@ --check test010.idr
3+idris $@ --check test010a.idr
4+idris $@ --check test010b.idr
55
66rm -f *.ibc