You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I've noticed that the sany script always returns 0 error code even if there are e.g. parse errors in the input file. E.g. I would like it to return a non-zero code to use it in the test suite of a transpiler targeting TLA+ I'm working on. By the way, thank you for tla-bin!
The text was updated successfully, but these errors were encountered:
Hi, thank you for the report. It looks like if one passes the -error-codes argument to sany on the nightly build then it will do exactly as you request. I've just added a --nightly flag to the download script which will install this.
Looks like they added this command line argument four months after this PR was filed! tlaplus/tlaplus#483
I've noticed that the
sany
script always returns0
error code even if there are e.g. parse errors in the input file. E.g. I would like it to return a non-zero code to use it in the test suite of a transpiler targeting TLA+ I'm working on. By the way, thank you fortla-bin
!The text was updated successfully, but these errors were encountered: