From f61ab9ac8c9812bed67c234a677593b182659b3f Mon Sep 17 00:00:00 2001
From: Tommaso Pecorella <tommaso.pecorella@unifi.it>
Date: Sun, 11 Dec 2022 12:58:45 +0100
Subject: [PATCH] doc: always report the warnings at end of doxygen check

---
 doc/doxygen.warnings.report.sh | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/doc/doxygen.warnings.report.sh b/doc/doxygen.warnings.report.sh
index 6eb6b22d0..ab2974b63 100755
--- a/doc/doxygen.warnings.report.sh
+++ b/doc/doxygen.warnings.report.sh
@@ -559,6 +559,12 @@ if [ "$filterin" != "" ] ; then
     echo "Filtered Warnings"
     echo "========================================"
     echo "$filterin"
+elif [ "$filter_log_results" != "" ] ; then
+    echo
+    echo
+    echo "Warnings"
+    echo "========================================"
+    echo "$filter_log_results"
 fi
 
 status_report 0 $me