tree 25f08cc4623c45b117728a3c47959374111b3d47
parent 7832c9fc3da624aa69c3d7436a154010e0c58386
author Gilles Peskine <Gilles.Peskine@arm.com> 1554735656 +0200
committer Gilles Peskine <Gilles.Peskine@arm.com> 1554914513 +0200

Clarify comment mangled by an earlier refactoring