Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
  2. clarified lines: like split_lines;
Changeset 67547:aefe7a7b330a by wenzelm:
clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
The file was modified src/Pure/General/pretty.scala (diff)
The file was modified src/Tools/Graphview/graphview.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
The file was modified src/Tools/jEdit/src/pretty_text_area.scala (diff)
The file was modified src/Tools/jEdit/src/pretty_tooltip.scala (diff)
Changeset 67546:2b30e03a7229 by wenzelm:
clarified lines: like split_lines;
The file was modified src/Tools/jEdit/src/pretty_tooltip.scala (diff)