removing an extension

Nick Pollitt writes:
 > I added an extension, and found later that I had made a mistake.
 > I want to reinstall the extension without removing all the others
 > (by obliterating .jigidx) yet I haven't found a way to do this -
 > I see no 'remove' button on the /Admin/Extensions page.  Is there
 > some 'clean' way to do this?

Check the check box of the extension you want to remove on the
/Admin/Extensions page, and press Ok. This should remove the
extension. It will not remove files already indexed by this extension,
however (this is a feature for me, but I can understand why someone
would consider this a bug).

Anselm.