Merge commit '598f0909568a51de8a2d1148f55a644fd8dffad0' into sync_cg_clif-2023-01-24

[rust.git] / src / ci / run.sh

diff --git a/src/ci/run.sh b/src/ci/run.sh
index b64300277508dd15af81644f540beca9ccafbcfb..0db9c993eecb407f2fd72cb4a3a0a76ef3535cb4 100755 (executable)
--- a/src/ci/run.sh
+++ b/src/ci/run.sh
@@ -184,11 +184,11 @@ if [ "$RUN_CHECK_WITH_PARALLEL_QUERIES" != "" ]; then
   $SRC/configure --set rust.parallel-compiler
 
   # Save the build metrics before we wipe the directory
-  if [ $HAS_METRICS = 1 ]; then
+  if [ "$HAS_METRICS" = 1 ]; then
     mv build/metrics.json .
   fi
   rm -rf build
-  if [ $HAS_METRICS = 1 ]; then
+  if [ "$HAS_METRICS" = 1 ]; then
     mkdir build
     mv metrics.json build
   fi