check if the valgrind report is about citus

pull/6660/head
Ahmet Gedemenli 2023-01-27 14:44:56 +03:00
parent 0ba273a11d
commit 229fed268c
1 changed files with 6 additions and 2 deletions

View File

@ -49,9 +49,13 @@ then
"$DIFF" -w $args "$file1.modified" "$file2.modified" | LC_CTYPE=C.UTF-8 diff-filter "$BASEDIR/normalize.sed" "$DIFF" -w $args "$file1.modified" "$file2.modified" | LC_CTYPE=C.UTF-8 diff-filter "$BASEDIR/normalize.sed"
diff_status=${PIPESTATUS[0]} diff_status=${PIPESTATUS[0]}
if [ -s "$BASEDIR/../citus_valgrind_test_log.txt" ]; then if [ -s "$BASEDIR/../citus_valgrind_test_log.txt" ]; then
if grep -q citus "$BASEDIR/../citus_valgrind_test_log.txt"; then
cat "$BASEDIR/../citus_valgrind_test_log.txt" cat "$BASEDIR/../citus_valgrind_test_log.txt"
exit 1 exit 1
fi fi
# if the file doesn't contain "citus", it's probably reported because of a pg issue
# we are currently not interested in such reports
fi
exit $diff_status exit $diff_status
else else
exec "$DIFF" -w $args "$file1" "$file2" exec "$DIFF" -w $args "$file1" "$file2"