I was surprised to discover this: $ time ./bash -c : $(seq 1000) 0.01s wall 0.00s user 0.00s system $ time ./bash -c : $(seq 10000) 0.40s wall 0.39s user 0.00s system $ time ./bash -c : $(seq 20000) 1.32s wall 1.31s user 0.01s system $ time ./bash -c : $(seq 40000) 4.57s wall 4.54s user 0.02s system
That's a fresh build of bash 4.4.18. None of the other shells I have handy exhibit this (zsh, ksh, dash). The trouble seems to be that bind_args() reverses argv, which means that push_args() has to insert each element from the left.
