Apparently I don't have permission to push to this repository.
I am attaching a patch which does what I suggested.  It looks to me
like it will work.

Ashok, can you give me write permission on this repository?  If so,
would you please?

Thanks.