> => done. Ready for review. BTW I don't know if we want
> a copyright in this trivial file (# is the comment char).

This looks fine and I'm tempted to just merge it, but Mukund, can you
confirm that it fixes the problem first?