On 12-06-20 13:50 , Diego Novillo wrote:

OK.  I suppose you do not have write to the repo, so I will commit it
for you.

Committed r188841.


Diego.

Reply via email to