chore: add comment

This commit is contained in:
Leonardo de Moura 2020-05-15 11:26:24 -07:00
parent d4aea2453a
commit e6463903d8

View file

@ -25,6 +25,7 @@ function compile_lean {
leanc -O3 -DNDEBUG -o "$f.out" "$@" "$f.c" || fail "Failed to compile C file $f.c"
}
# Remark: `${var+x}` is a parameter expansion which evaluates to nothing if `var` is unset, and substitutes the string `x` otherwise.
function exec_check {
ret=0
[ -n "${expected_ret+x}" ] || expected_ret=0