This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 55 - Paste onto empty line gives wrong font.
Summary: Paste onto empty line gives wrong font.
Status: CLOSED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: GUI (show other bugs)
Version: 3.3.38
Hardware: All All
: P3 normal
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2003-09-10 20:53 CEST by Ulrik Nyman
Modified: 2004-06-11 09:50 CEST (History)
0 users

See Also:
Architecture:

Attachments
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
Description Ulrik Nyman 2003-09-10 20:53:38 CEST 
When pasting text into an empty line in the bottom of the declarations editor
(e.g. when editing  the global declarations). The pasted is printed in a non
fixed width font instead of the fixed width font generally used in the
declarations editor.
The font changes to the correct one after change the focus to another component
and back again or when syntax checking.
Comment 1 Gerd Behrmann 2004-03-14 12:56:49 CET 
A fix has been checked into CVS.