From 45f35943ac1bce8ee2a97fcdd8caf8b0862302d0 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 6 Jul 2022 17:56:30 +0200
Subject: [PATCH] [Script] bin/test.sh - minor change
---
bin/test.sh | 20 ++++++++++++--------
1 file changed, 12 insertions(+), 8 deletions(-)
diff --git a/bin/test.sh b/bin/test.sh
index 24b8d54c77c..a08a3d356c3 100755
--- a/bin/test.sh
+++ b/bin/test.sh
@@ -30,8 +30,8 @@ TESTS=
SAVE=
DUNE_OPT=
-DUNE_LOG=.test-errors.log
-
+DUNE_LOG=./.test-errors.log
+CACHEDIR=./.wp-cache
FRAMAC_WP_CACHE_GIT=git@git.frama-c.com:frama-c/wp-cache.git
# --------------------------------------------------------------------------
@@ -130,14 +130,18 @@ function SetEnv
FRAMAC_WP_CACHE=offline
Echo "Set FRAMAC_WP_CACHE=$FRAMAC_WP_CACHE"
fi
+
if [ "$FRAMAC_WP_QUALIF" != "" ]; then
- FRAMAC_WP_CACHEDIR=$FRAMAC_WP_QUALIF
- else
- if [ "$FRAMAC_WP_CACHEDIR" = "" ]; then
- FRAMAC_WP_CACHEDIR=./.wp-cache
- Echo "Set FRAMAC_WP_CACHEDIR=$FRAMAC_WP_CACHEDIR"
- fi
+ FRAMAC_WP_CACHEDIR="$FRAMAC_WP_QUALIF"
+ Echo "Set FRAMAC_WP_CACHEDIR=$FRAMAC_WP_CACHEDIR"
+ elif [ "$FRAMAC_WP_CACHEDIR" = "" ]; then
+ FRAMAC_WP_CACHEDIR="$CACHEDIR"
+ Echo "Set FRAMAC_WP_CACHEDIR=$FRAMAC_WP_CACHEDIR"
fi
+
+ [ ! -f "$FRAMAC_WP_CACHEDIR" ] || [ -d "$FRAMAC_WP_CACHEDIR" ] \
+ || Error "$FRAMAC_WP_CACHEDIR is not a directory"
+
}
function CloneCache
--
GitLab