jdom/no-jaxen.patch

12 lines
534 B
Diff

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>"