BTW, should we fix the mixed indentation style in these lines (tabs
vs. spaces)?

Michael.