update_diff script

diff --git a/tests/examples/update_diffs.sh b/tests/examples/update_diffs.sh
index 9278df98acd37a1c20eeb3f210653611c4e455f8..afae4093f63380eb6264c62342fad1a33b042306 100755 (executable)
--- a/tests/examples/update_diffs.sh
+++ b/tests/examples/update_diffs.sh
@@ -34,8 +34,7 @@ for file in ${diff_files}; do
     echo diff "${source_file}" "${modified_file}" \> "${file}"
     diff "${source_file}" "${modified_file}" > "${file}"
   else
-    echo "No matching .cc files found for ${file}"
-    exit 1
+    echo "No matching .cc files found for ${file}: source=${source_file} modified=${modified_file}"
   fi
 done