Hurrah, even more use of «». But that is okay, as I have nearly half of my terminals configured now, so that I can input and view them.
I don't understand why it is needed, though. Why wasn't infix:+ good enough? infix:«+» and infix:{'+'} are more linenoise, and IMHO it's far from elegant. Juerd