Closed laverdet closed 5 years ago
I clobbered my working directory a while ago and eventually forgot that I wrote this. I just went to write it again but discovered I had already written it. Anyway the commit is rebased if you want to consider merging it still.
Merged to ptr
branch. It will be merged to master in a few days, so this PR can still remain open.
This is a useful feature.