git.iko.soy/Idris-dev
on cd58dfb help sign in
Idris-dev/test/interactive015/run
8 lines 173 B history raw
1#!/usr/bin/env bash
3cp src/interactive015.idr .
4${IDRIS:-idris} "$@" --quiet --port none interactive015.idr < input
6cat interactive015.idr
8rm -f *.ibc interactive015.idr