run: remove now unneeded || true
This commit is contained in:
parent
d1720c42e4
commit
42163fab17
29 changed files with 29 additions and 29 deletions
|
@ -1,2 +1,2 @@
|
|||
cat > Main.idr
|
||||
idris --execute ./Main.idr || true
|
||||
idris --execute ./Main.idr
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue