Paolo Carlini wrote: > Hi, > > working on 12077 I noticed this include, which seems redundant. > Indeed, I removed it and successfully regtested. Forget about this, sorry. However, we could probably include much less... Paolo.