Closed fnothaft closed 7 years ago
Indeed! 'tis quite useful.
@fnothaft — Since this PR essentially includes #94 , how do you want to handle it?
Whatever's easiest for you! If you want to merge this, then you don't need to independently review and merge #94.
Adds the following sorters and duplicate markers for benchmarking purposes:
A couple of commits are spuriously getting included...