diff --git a/.github/workflows/docs_update.yml b/.github/workflows/docs_update.yml
index 277014cc05..3b6bdc79ed 100644
--- a/.github/workflows/docs_update.yml
+++ b/.github/workflows/docs_update.yml
@@ -45,7 +45,7 @@ jobs:
         run: |
           ./regen.sh php
           if [[ -s doxygen.log ]]; then
-            echo '*** There were warnings during docs generation: ***'
+            echo 'Contents of Doxygen log file follows:'
             echo '-----------------------------------------------------------'
             cat doxygen.log
             echo '-----------------------------------------------------------'
diff --git a/.gitignore b/.gitignore
index aecf49e324..17bcc0d809 100644
--- a/.gitignore
+++ b/.gitignore
@@ -157,7 +157,6 @@
 /distrib/release
 
 # /docs/doxygen/
-/docs/doxygen/doxygen.log
 /docs/doxygen/out
 
 # /include/
diff --git a/docs/doxygen/regen.sh b/docs/doxygen/regen.sh
index ad9f6e4f98..5b158c86d5 100755
--- a/docs/doxygen/regen.sh
+++ b/docs/doxygen/regen.sh
@@ -239,5 +239,12 @@ fi
 # Doxygen has the annoying habit to put the full path of the
 # affected files in the log file; remove it to make the log
 # more readable
-topsrcdir=`cd ../.. && pwd`
-sed -i'' -e "s|$topsrcdir/||g" doxygen.log
+if [[ -s doxygen.log ]]; then
+    topsrcdir=`cd ../.. && pwd`
+    sed -i'' -e "s|$topsrcdir/||g" doxygen.log
+
+    echo '*** There were warnings during docs generation ***'
+else
+    # Don't leave empty file lying around.
+    rm doxygen.log
+fi