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

Bug 55

Summary: Paste onto empty line gives wrong font.
Product: UPPAAL Reporter: Ulrik Nyman <ulrik>
Component: GUIAssignee: Gerd Behrmann <behrmann>
Status: CLOSED FIXED    
Severity: normal    
Priority: P3    
Version: 3.3.38   
Hardware: All   
OS: All   
Architecture:

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.