From 1739802361492e09cccc480cbebdb2cd78513f4b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 3 Oct 2023 19:54:35 +0200
Subject: [PATCH] [tests] force dune tests
---
bin/test.sh | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/bin/test.sh b/bin/test.sh
index 35d0939f177..f0aab532878 100755
--- a/bin/test.sh
+++ b/bin/test.sh
@@ -71,6 +71,7 @@ function Usage
echo " -r|--clean clean (remove all) test results (includes -p)"
echo " -p|--ptests prepare (all) dune files"
echo " -w|--wp-cache prepare (pull) WP-cache"
+ echo " -f|--force force re-run tests"
echo " -l|--logs print output of tests (single file, no diff)"
echo " -u|--update run tests and update oracles (and WP-cache)"
echo " -k|--commit commit new test oracles"
@@ -158,6 +159,9 @@ do
"-w"|"--wp-cache")
PULLCACHE=yes
;;
+ "-f"|"--force")
+ DUNE_OPT+="--force "
+ ;;
"-u"|"--update")
DUNE_OPT+="--auto-promote "
UPDATE=yes
--
GitLab