From d5dd7209fca1ed9da298f02ae5ae499e7a1f88c6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 30 Jun 2022 18:13:18 +0200
Subject: [PATCH] [dune] fix ./bin/test help on variables
---
bin/test.sh | 43 ++++++++++++++++++++++---------------------
1 file changed, 22 insertions(+), 21 deletions(-)
diff --git a/bin/test.sh b/bin/test.sh
index 23b1055d1c8..247dbe70dc8 100755
--- a/bin/test.sh
+++ b/bin/test.sh
@@ -21,6 +21,7 @@
# #
##########################################################################
+THIS_SCRIPT="$0"
CONFIG="<all>"
VERBOSE=
UPDATE=
@@ -34,9 +35,9 @@ FRAMAC_WP_CACHE_GIT=git@git.frama-c.com:frama-c/wp-cache.git
# --- Help Message
# --------------------------------------------------------------------------
-THIS_SCRIPT="$0"
function Usage
{
+ SetEnv
echo "USAGE"
echo ""
echo "${THIS_SCRIPT} [OPTIONS|TESTS]..."
@@ -65,13 +66,13 @@ function Usage
echo ""
echo "VARIABLES"
echo ""
- echo " FRAMAC_WP_CACHEDIR=$FRAMAC_WP_CACHEDIR"
- echo " Git URL: $FRAMAC_WP_CACHE_GIT"
- echo " Please, always push updates to #master branch"
- echo ""
- echo " FRAMAC_WP_CACHE=$FRAMAC_WP_CACHE"
+ echo " FRAMAC_WP_CACHE ($FRAMAC_WP_CACHE)"
echo " Management mode of wp-cache"
echo ""
+ echo " FRAMAC_WP_CACHEDIR ($FRAMAC_WP_CACHEDIR)"
+ echo " Use $FRAMAC_WP_CACHE_GIT"
+ echo " Please, always push to master branch"
+ echo ""
}
# --------------------------------------------------------------------------
@@ -117,20 +118,6 @@ function Cmd
# --- WP Cache Environment
# --------------------------------------------------------------------------
-function CloneCache
-{
- if [ ! -d "$FRAMAC_WP_CACHEDIR" ]; then
- Head "Cloning WP cache..."
- Cmd git clone $FRAMAC_WP_CACHE_GIT $FRAMAC_WP_CACHEDIR
- fi
-}
-
-function PullCache
-{
- Head "Pull WP cache..."
- Run git -C $FRAMAC_WP_CACHEDIR pull --rebase
-}
-
function SetEnv
{
if [ "$FRAMAC_WP_CACHE" = "" ]
@@ -144,8 +131,20 @@ function SetEnv
FRAMAC_WP_CACHEDIR=./.wp-cache
Echo "Set FRAMAC_WP_CACHEDIR=$FRAMAC_WP_CACHEDIR"
fi
+}
- CloneCache
+function CloneCache
+{
+ if [ ! -d "$FRAMAC_WP_CACHEDIR" ]; then
+ Head "Cloning WP cache..."
+ Cmd git clone $FRAMAC_WP_CACHE_GIT $FRAMAC_WP_CACHEDIR
+ fi
+}
+
+function PullCache
+{
+ Head "Pull WP cache..."
+ Run git -C $FRAMAC_WP_CACHEDIR pull --rebase
}
# --------------------------------------------------------------------------
@@ -154,6 +153,7 @@ function SetEnv
function TestDir
{
+ CloneCache
case "$CONFIG" in
"<all>")
ALIAS=$1/ptests
@@ -175,6 +175,7 @@ function TestDir
function TestFile
{
+ CloneCache
DIR=$(dirname $1)
FILE=$(basename $1)
[ "$CONFIG" != "<all>" ] || \
--
GitLab