>>>>> "Lars" == Lars Gullik Bjønnes <[EMAIL PROTECTED]> writes:
Lars> And pretty simple it was too. What remains to see is whether this change will prove helpful when we actually need proper identifiers... Lars> Sorry for being such a drag about this, but I thought it Lars> important. Lars> btw. This is ok for 1.4 as well. You mean I'm supposed to do it? Bummer. JMarc
