Quelle  line_separator   Sprache: unbekannt

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();