wenzelm [Thu, 30 Jan 2025 21:44:44 +0100] rev 82022
more thorough cleanup;
wenzelm [Thu, 30 Jan 2025 20:55:42 +0100] rev 82021
more options for build_release: support bundled browser_info and Find_Facts database;
wenzelm [Thu, 30 Jan 2025 13:16:51 +0100] rev 82020
more standard directory structure;
wenzelm [Thu, 30 Jan 2025 13:13:21 +0100] rev 82019
tuned output;
wenzelm [Thu, 30 Jan 2025 11:53:26 +0100] rev 82018
suppress MacOS.jar from jEdit 5.7.0, following 65fd0f032a75;
wenzelm [Wed, 29 Jan 2025 21:25:44 +0100] rev 82017
tuned GUI: attempt to improve divider mobility;
wenzelm [Wed, 29 Jan 2025 20:52:27 +0100] rev 82016
rebuild jedit component;
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;
wenzelm [Wed, 29 Jan 2025 14:43:14 +0100] rev 82014
more accurate syntax: follow documentation in "isar-ref" (and command 'syntax_consts');
wenzelm [Wed, 29 Jan 2025 11:53:49 +0100] rev 82013
more robust: make double sure that buffer.getText() is valid (see also 2e7073976c25);