From cd8a233855d4358aba91d4b8d6bcfa0c7c6b4dea Mon Sep 17 00:00:00 2001 From: David Raymond Christiansen Date: Tue, 6 May 2014 19:55:20 +0200 Subject: [PATCH] Don't try to compile a test that doesn't have `main` Instead, just --check it. --- test/totality001/run | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/totality001/run b/test/totality001/run index 4a150af2b..7092f8da1 100755 --- a/test/totality001/run +++ b/test/totality001/run @@ -1,6 +1,6 @@ #!/usr/bin/env bash -idris $@ test010.idr -o test010 -idris $@ test010a.idr -o test010 -idris $@ test010b.idr -o test010 +idris $@ --check test010.idr +idris $@ --check test010a.idr +idris $@ --check test010b.idr rm -f *.ibc