Pushed as 62d4295389. Thanks for the quick check! (And the reminder to eternal vigilance.) -JimC -- James Cloos <cloos at jhcloos.com> OpenPGP: 1024D/ED7DAEA6