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

Re:removing an extension

From: Alexandre Rafalovitch <alex@access.com.au>
Date: Tue, 27 Aug 1996 09:29:37 +1000
Message-Id: <v02140b00ae47e2e869cc@[]>
To: www-jigsaw@w3.org (jigsaw list)
At 5:12 AM 27/8/96, Nick Pollitt wrote:
>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?

There is a remove button, it just does not advertise itself.:-{  On the
extensions page there is a checkbox for each extension. If you will select
those checkboxes and click Ok, selected extensions will be removed.

Hope it helps,
Ps, All the resources that already used your extension information would
have to be reindexed/deleted-restored so they can take advantage of new
extension information. Otherwise they would just keep erroneous values. :-{

Received on Monday, 26 August 1996 19:30:08 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:25:29 UTC