myriad/languages/idris/run.sh

cat > Main.idr
idris --execute ./Main.idr
eval: limit docker output to not run out of memory 2020-06-07 09:43:41 +02:00			`cat > Main.idr`
run: remove now unneeded `\|\| true` 2020-06-17 07:43:31 +02:00			`idris --execute ./Main.idr`