git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/regression002/run
38 lines 679 B history raw
1#!/usr/bin/env bash
3${IDRIS:-idris} $@ --nobanner --nocolour --quiet --port none <<!
4:load reg003.idr
5:load reg003a.idr
6:load reg006.idr
7:load reg007.lidr
8:load reg010.idr
9:load reg018a.idr
10:load reg018b.idr
11:load reg018c.idr
12:load reg018d.idr
13:load reg023.idr
14:load reg028.idr
15:load reg028a.idr
16:load reg034.idr
17:load reg035.idr
18:load reg035a.lidr
19:load reg035b.idr
20:load reg044.idr
21:load reg049.idr
22:load working.idr
23:load badbangop.idr
24:load baddoublebang.idr
25:load reg054.idr
26:load reg055.idr
27:load reg055a.idr
28:load reg056.idr
29:load reg068.idr
30:load reg069.idr
31:load reg070.idr
32:load reg076.idr
33:load reg077.idr
34:load DoubleEquality.idr
35:load Canonicity.idr
38rm -f *.ibc