diff -urEbwB jdom/build.xml jdom.new/build.xml
--- jdom/build.xml	2012-02-26 00:30:45.000000000 +0100
+++ jdom.new/build.xml	2023-08-23 19:35:51.544436993 +0200
@@ -254,6 +255,7 @@
              use="true"
              splitindex="true"
              noindex="false"
+             failonerror="false"
              windowtitle="${Name} v${version}"
              doctitle="${Name} v${version}<br>API Specification"
              header="<b>${Name}<br><font size='-1'>${version}</font></b>"