ROIBrush tool

[dscho]

Hi list,

I have the pleasure to announce the ROI Brush tool. Just start this
plugin, and a new tool will appear: the ROI Brush. It works like a brush,
but instead of painting circular regions, it _selects_ them (or, if you
press Alt or Shift while dragging the mouse, _deselects_ them).

This plugin was contributed by Tom Larkworthy, who granted me permission
to release it into the wild.

Ciao,
Dscho