"Ross Paterson" <ross@soi.city.ac.uk> writes: > > Can we now get rid of -i and :project? Yes, I think that's a reasonable code simplification to make; I doubt there are users of either feature nowadays. Anyway, I'm in the middle of making a code change that tidies up the handling of options, so perhaps you could wait until then? Couple of hours away from committing, I reckon. --sigbjorn