removing an extension

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?

Nicholas Pollitt            |  If you know the enemy and know
NCSA                        |  yourself, you need not fear the 
Software Development Group  |  result of a hundred battles.
npollitt@ncsa.uiuc.edu      |  -- Sun Tzu

Received on Monday, 26 August 1996 15:16:51 UTC