W3C home > Mailing lists > Public > www-jigsaw@w3.org > July to August 1996

removing an extension

From: Anselm Baird-Smith <abaird@w3.org>
Date: Mon, 26 Aug 1996 20:29:26 +0500
Message-Id: <9608270029.AA11845@www18.w3.org>
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 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 9 April 2012 12:13:25 GMT