[metapost] drawdot issue

[Stephan Hennig]

schrieb Stephan Hennig:

> it is also stroked with the pen given to withpen.  Which makes for a
> dot that is too large.

That is incorrect.  The circle size corresponds to that of the withpen
statement (as can be seen from the second variant), but the stroke is
drawn with the currently active pen.  While there shouldn't be a stroke
at all.

Best regards,
Stephan Hennig