> On 5 Feb 2015, at 23:43, Sebastiano Vigna <vi...@di.unimi.it> wrote: > > >> On 5 Feb 2015, at 22:24, Dmitriy Lyubimov <dlie...@gmail.com> wrote: >> >> thank you very much. >> >> Github pull request is what we use these days. Do you think you could put >> one up ? > > I did it, and I hope is fine. Can you check? Sorry, it's my first fork/pull...
Just curious, did anybody test whether some higher-level task are faster? Ciao, seba