2026-05-20

Echo to stderr

echoerr() { echo "$@" 1>&2; }