git.iko.soy/Idris-dev
on master help sign in
Idris-dev/test/pkg008/run.sh
11 lines 302 B history raw
1#!/usr/bin/env bash
3${IDRIS:-idris} $@ --build maths.ipkg
4${IDRIS:-idris} $@ --testpkg maths.ipkg | grep -v -e "idris"
6# Idris only appears in the randomly generated name of test so we grep
7# to remove it to make output consistent.
9${IDRIS:-idris} $@ --clean maths.ipkg
11${IDRIS:-idris} $@ -p maths