Browse Source

Added wrapping to MultipleLineStringEditor, e.g. in graph title setting.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@140 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 20 years ago
parent
commit
ae64d59ad7
  1. 1
      prism/src/settings/MultipleLineStringEditor.java

1
prism/src/settings/MultipleLineStringEditor.java

@ -48,6 +48,7 @@ public class MultipleLineStringEditor implements SettingEditor, KeyListener, Car
public MultipleLineStringEditor()
{
area = new JTextArea();
area.setLineWrap(true);
font = new Font("monospaced", Font.PLAIN, 12);
area.addCaretListener(this);

Loading…
Cancel
Save