SunRed/myriad
1
0
Fork 0
Code Issues Pull requests Packages Projects Releases Wiki Activity
myriad/languages/idris/run.sh
1computer1 42163fab17 run: remove now unneeded || true
2020-06-17 01:43:31 -04:00

3 lines
42 B
Bash
Raw Blame History

cat > Main.idr
idris --execute ./Main.idr
Reference in a new issue View git blame Copy permalink