File jedit-encoding.patch of Package jedit

--- jEdit/build.xml	2017-09-19 00:37:45.034686782 +0200
+++ jEdit/build.xml	2017-09-19 00:45:49.916917830 +0200
@@ -790,7 +790,8 @@
 					 source="${target.java.version}"
 					 encoding="UTF-8"
 					 docencoding="UTF-8"
-					 charset="UTF-8">
+					 charset="UTF-8"
+					 additionalparam="-J-Dfile.encoding=UTF-8">
 					<group title="jEdit 5 API"
 					       packages="org.jedit.*"/>					       
 					<group title="jEdit 4 API"