On Mon, Jan 18, 2016 at 10:37:23PM -0500, Guillaume Munch wrote: > > Enrico: the width of the line of the plain separator changed, as you can > see, which I guess was not intended.
For the new symbol I used the width of 'n' instead of 'm'. As both kind share the same base width, I tried to compensate choosing the width of the plain separator as 8 times the width of 'n', while it previously was 5 times the width of 'm'. I didn't care to measure the widths as I deemed it not so important. Note also that this is font dependent. You are welcome to suggest something different than 8 if you find it is too large or too narrow with respect to the previous width. -- Enrico
