- From: Anselm Baird-Smith <abaird@w3.org>
- Date: Mon, 26 Aug 1996 20:29:26 +0500
- To: npollitt@ncsa.uiuc.edu (Nick Pollitt)
- Cc: www-jigsaw@w3.org (jigsaw list)
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.
Received on Monday, 26 August 1996 20:29:30 UTC