tla-bin
tla-bin copied to clipboard
pmer
sany: return non-zero exit code if there are errors
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!
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! https://github.com/tlaplus/tlaplus/pull/483
Please share if this works for your use case!
