-
Type:
Bug
-
Resolution: Fixed
-
Priority:
P3
-
Affects Version/s: 9
-
Component/s: tools
-
b142
-
Not verified
Generated file should end in ".java" for editors (like jEdit) which key formatting off the filename extension.