On the topic of filtering, I wonder if it would make sense to support an API that would allow filtering by file extension instead of regexps. I'm guessing that sort of filter could be implemented much more efficiently than with regexps, and I'll bet its a very common use case. Something like myfilter.exts = ["ml", "mli", "mll", "mly"]
On the topic of filtering, I wonder if it would make sense to support an API that would allow filtering by file extension instead of regexps. I'm guessing that sort of filter could be implemented much more efficiently than with regexps, and I'll bet its a very common use case. Something like
myfilter.exts = ["ml", "mli", "mll", "mly"]