[#2793] fix a mistake in JSON CI script that made it check all files when none were...

diff --git a/tools/check-for-json-errors-in-doc.sh b/tools/check-for-json-errors-in-doc.sh
index a748cfb07d87366e6533c6bff5c794de91f1dd1c..732ac90b2612e8a997cef3078391ae954900bf72 100755 (executable)
--- a/tools/check-for-json-errors-in-doc.sh
+++ b/tools/check-for-json-errors-in-doc.sh
@@ -17,6 +17,11 @@ if test ${#} -gt 0; then
 else
        # By default, check only modified files.
        files=$(git diff --name-only $(git merge-base origin/master HEAD))
+
+       # If there is nothing to check, exit early. Otherwise, it checks everything.
+       if test -z "${files}"; then
+               exit 0
+       fi
 fi
 
 exit_code=0