git.iko.soy/Idris-dev
on ebb4fee help sign in
Idris-dev/test/pkg008/run
9 lines 273 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