13 Nov
2018
13 Nov
'18
1:53 p.m.
On 13/11/2018 10:46, osm@pinns wrote:
I forgot to check this with r4251 which indeed reports wrong linewidth!
Are you sure? I don't think it does! You are right and it needs a check as the width is not saved anywhere so it must be 32. Here is a patch to add the check. Steve