Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. less aggressive default position: prefer persistent defaults maintained by jEdit (amending 89c5bb2a2128);
Changeset 66605:261dcd52c5a0 by wenzelm:
less aggressive default position: prefer persistent defaults maintained by jEdit (amending 89c5bb2a2128);
The file was modified src/Pure/PIDE/line.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_editor.scala (diff)