From d46149dec0cbd0a707c011b9edd2ae95f49c4773 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 19 Apr 2024 17:21:34 +0200
Subject: [PATCH] [tests] Also promote err.log files
---
bin/test.sh | 40 ++++++++++++++++++++++++----------------
1 file changed, 24 insertions(+), 16 deletions(-)
diff --git a/bin/test.sh b/bin/test.sh
index 8d3944c2eae..9da5fb9db7d 100755
--- a/bin/test.sh
+++ b/bin/test.sh
@@ -500,27 +500,35 @@ function Register
# --- Tests Create New Oracles
# --------------------------------------------------------------------------
+function CreateNewOraclesAux
+{
+ for log in $1*.$2.log
+ do
+ # Only non-empty oracles
+ if [ -s "$log" ];
+ then
+ dest="${log//result/oracle}"
+ dest="${dest//$2.log/$2.oracle}"
+ # Only non-existing oracles, existing ones will be updated via
+ # dune --auto-promote
+ if [ ! -f "../../$dest" ];
+ then
+ echo "Create oracle $dest"
+ cp -f $log "../../$dest"
+ fi
+ fi
+ done
+}
+
function CreateNewOracles
{
while [ "$1" != "" ]
do
cd _build/default
- for log in $1*.res.log
- do
- # Only non-empty oracles
- if [ -s "$log" ];
- then
- dest="${log//result/oracle}"
- dest="${dest//res.log/res.oracle}"
- # Only non-existing oracles, existing ones will be updated via
- # dune --auto-promote
- if [ ! -f "../../$dest" ];
- then
- echo "Create oracle $dest"
- cp -f $log "../../$dest"
- fi
- fi
- done
+
+ CreateNewOraclesAux $1 res
+ CreateNewOraclesAux $1 err
+
cd ../..
shift
done
--
GitLab