| Wed, 29 Jan 2025 20:52:27 +0100 | wenzelm | rebuild jedit component; | changeset | files |
| Wed, 29 Jan 2025 20:17:21 +0100 | wenzelm | 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; | changeset | files |
| Wed, 29 Jan 2025 14:43:14 +0100 | wenzelm | more accurate syntax: follow documentation in "isar-ref" (and command 'syntax_consts'); | changeset | files |