ciscript: don't use an empty string as a number

An empty string is not a valid number, and some shells complain.

Check instead if $COVERITY is non-empty, which is a common convention
and what we're doing anyway.

diff --git a/script/cibuild.sh b/script/cibuild.sh
index 1f15e851e36345b0662415311b7c2f3067e578d2..699404bd2126ecf3e04a85e001c23eb46cabd980 100755 (executable)
--- a/script/cibuild.sh
+++ b/script/cibuild.sh
@@ -1,6 +1,6 @@
 #!/bin/sh
 
-if [ "$COVERITY" -eq 1 ];
+if [ -n "$COVERITY" ];
 then
        ./script/coverity.sh;
        exit $?;