On vacation

[Julian Hyde]

I’m on vacation for the next week, pretty much offline. I’d appreciate if 
someone could review PRs, etc. 

Julian