@ernest just merge rev. 3700 of the proposed branch. Another revision was added later, undoing the fix.
@ernest just merge rev. 3700 of the proposed branch. Another revision was added later, undoing the fix.