Hi, Kevin Cozens <kcozens@xxxxxxxxxxxx> writes: > This is too trivial to bugzilla so I'll just mention it here. All bugs are supposed to be filed in Bugzilla. For bugs that might need some additional discussion, you should post here as well. Trivial bugs such as the one you mentioned can be handled in Bugzilla only. But thanks for spotting this problem and reporting it. I will check in the fix later. Sven
