]> https://gitweb.dealii.org/ - dealii.git/commitdiff
update_diff script 17116/head
authorTimo Heister <timo.heister@gmail.com>
Mon, 10 Jun 2024 19:13:07 +0000 (15:13 -0400)
committerTimo Heister <timo.heister@gmail.com>
Mon, 10 Jun 2024 19:13:24 +0000 (15:13 -0400)
tests/examples/update_diffs.sh

index 9278df98acd37a1c20eeb3f210653611c4e455f8..afae4093f63380eb6264c62342fad1a33b042306 100755 (executable)
@@ -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
 

In the beginning the Universe was created. This has made a lot of people very angry and has been widely regarded as a bad move.

Douglas Adams


Typeset in Trocchi and Trocchi Bold Sans Serif.