Am 08.10.19 um 14:04 schrieb Johannes Schindelin: > So you got what you wished for: > https://public-inbox.org/git/pull.378.git.gitgitgad...@gmail.com
After having seen the result I do not wish for it anymore. (Not that I had "wished" for it in the first place...) It does not make the result any more readable than the original. I do wish you had rejected Junio's suggestion to introduce index_pos_to_insert_pos(). It doesn't make the code a lot more readable, either, in my eyes. -- Hannes
