Skip to content
Snippets Groups Projects
Commit 45f35943 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[Script] bin/test.sh - minor change

parent da878535
No related branches found
No related tags found
No related merge requests found
...@@ -30,8 +30,8 @@ TESTS= ...@@ -30,8 +30,8 @@ TESTS=
SAVE= SAVE=
DUNE_OPT= 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 FRAMAC_WP_CACHE_GIT=git@git.frama-c.com:frama-c/wp-cache.git
# -------------------------------------------------------------------------- # --------------------------------------------------------------------------
...@@ -130,14 +130,18 @@ function SetEnv ...@@ -130,14 +130,18 @@ function SetEnv
FRAMAC_WP_CACHE=offline FRAMAC_WP_CACHE=offline
Echo "Set FRAMAC_WP_CACHE=$FRAMAC_WP_CACHE" Echo "Set FRAMAC_WP_CACHE=$FRAMAC_WP_CACHE"
fi fi
if [ "$FRAMAC_WP_QUALIF" != "" ]; then if [ "$FRAMAC_WP_QUALIF" != "" ]; then
FRAMAC_WP_CACHEDIR=$FRAMAC_WP_QUALIF FRAMAC_WP_CACHEDIR="$FRAMAC_WP_QUALIF"
else Echo "Set FRAMAC_WP_CACHEDIR=$FRAMAC_WP_CACHEDIR"
if [ "$FRAMAC_WP_CACHEDIR" = "" ]; then elif [ "$FRAMAC_WP_CACHEDIR" = "" ]; then
FRAMAC_WP_CACHEDIR=./.wp-cache FRAMAC_WP_CACHEDIR="$CACHEDIR"
Echo "Set FRAMAC_WP_CACHEDIR=$FRAMAC_WP_CACHEDIR" Echo "Set FRAMAC_WP_CACHEDIR=$FRAMAC_WP_CACHEDIR"
fi
fi fi
[ ! -f "$FRAMAC_WP_CACHEDIR" ] || [ -d "$FRAMAC_WP_CACHEDIR" ] \
|| Error "$FRAMAC_WP_CACHEDIR is not a directory"
} }
function CloneCache function CloneCache
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment