Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. make double-sure that refresh happens eventually, even without edits (e.g. height change) -- amending 8bf765c9c2e5;
  3. simplified;
  4. tuned;
Changeset 63775:fd6caec306fc by wenzelm:
merged
Changeset 63774:749794930d61 by wenzelm:
make double-sure that refresh happens eventually, even without edits (e.g. height change) -- amending 8bf765c9c2e5;
The file was modified src/Tools/jEdit/src/text_overview.scala (diff)
Changeset 63773:d1a5d10affc0 by wenzelm:
simplified;
The file was modified src/Pure/library.scala (diff)
Changeset 63772:4ad836f0b146 by wenzelm:
tuned;
The file was modified src/Tools/jEdit/src/keymap_merge.scala (diff)