>>>>> "Andre" == Andre Poenitz <[EMAIL PROTECTED]> writes:
Andre> On Tue, Feb 11, 2003 at 03:51:42PM +0100, Jean-Marc Lasgouttes Andre> wrote: >> So what should we do? Maybe remove the options altogether and use a >> plain "sort"? Would that give the same result for everybody? Andre> Do they need to be sorted at all? Yes, probably, so that we can uniquify the list. JMarc
