I don't know how good my git knowledge is, but if you send @takluyver a pull request with just this change in, he should be able to merge it in here. That said, the change is small enough @taklluyver could just cherry-pick it in :-)