Inconsistent behavior of indent-lines in jEdit

Balazs Toth balazs.toth at lmu.de
Sun May 31 16:34:07 CEST 2026


If I enable the setting "Restore previously open files on startup" and 
restart jEdit, then indenting lines (automatic on new line and via the 
short-cut) puts everything to the start of the lines.

I can consistently reproduce it on my MacBook.



Balazs



More information about the isabelle-dev mailing list