From e6463903d881fc5ffb6eef2b6fbcbc766367c80f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 15 May 2020 11:26:24 -0700
Subject: [PATCH] chore: add comment

---
 tests/common.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tests/common.sh b/tests/common.sh
index 0a7ea1e265..e7fa3e2544 100644
--- a/tests/common.sh
+++ b/tests/common.sh
@@ -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