# HG changeset patch
# User wenzelm
# Date 1738178241 -3600
# Node ID fe186fd7a168e45048663a9a0f4861ced7c21fd1
# Parent  8464b7f19c519b6fab3a92e4505b0be1c22566c9
make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;

diff -r 8464b7f19c51 -r fe186fd7a168 src/Tools/jEdit/patches/line_separator
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/line_separator	Wed Jan 29 20:17:21 2025 +0100
@@ -0,0 +1,23 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/bufferio/BufferIORequest.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/bufferio/BufferIORequest.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/bufferio/BufferIORequest.java	2024-08-03 19:53:19.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/bufferio/BufferIORequest.java	2025-01-29 20:03:36.236518733 +0100
+@@ -357,7 +357,7 @@
+ 
+ 		Segment lineSegment = new Segment();
+ 		String newline = buffer.getStringProperty(JEditBuffer.LINESEP);
+-		if(newline == null)
++		if(newline == null || newline.isEmpty())
+ 			newline = System.getProperty("line.separator");
+ 
+ 		final int bufferLineCount = buffer.getLineCount();
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/Buffer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/Buffer.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/Buffer.java	2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/Buffer.java	2025-01-29 20:00:53.025217244 +0100
+@@ -1236,6 +1236,7 @@
+ 	 */
+ 	public void setLineSeparator(String lineSep)
+ 	{
++		lineSep = org.jedit.misc.LineSepType.fromSeparator(lineSep).getSeparator();
+ 		setProperty(LINESEP, lineSep);
+ 		setDirty(true);
+ 		propertiesChanged();