Wed, 29 Jan 2025 20:52:27 +0100 rebuild jedit component;
wenzelm [Wed, 29 Jan 2025 20:52:27 +0100] rev 82016
rebuild jedit component;
Wed, 29 Jan 2025 20:17:21 +0100 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;
wenzelm [Wed, 29 Jan 2025 20:17:21 +0100] rev 82015
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;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 tip