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

Bug 412

Summary: Default filename when exporting template
Product: UPPAAL Reporter: Rasmus Jacobsen <rasseren>
Component: GUIAssignee: Marius Mikučionis <marius>
Status: RESOLVED FIXED    
Severity: enhancement    
Priority: P2    
Version: 4.0.5   
Hardware: PC   
OS: Linux   
Architecture:

Description Rasmus Jacobsen 2007-04-11 09:29:08 CEST 
Hi again

It would be nice if the name of the template was entered as default filename when exporting to eps.

Thanks Rasmus
Comment 1 Gerd Behrmann 2007-04-11 12:43:33 CEST 
Agreed. I think this change is minor enough, yet very useful, to allow it to be done on the stable branch. Marius, do you do it?
Comment 2 Marius Mikučionis 2007-04-11 19:33:08 CEST 
here, you have it in branch/4.0 :-)

now it dumps the picture to template.eps instead of stdout.

shall I update the trunk too?
Comment 3 Marius Mikučionis 2007-04-19 18:58:56 CEST 
it seems that version at trunk requires an explicit option for the filename, so I declare this bug as fixed.