Change back to /dev/stdin, even though it isn't portable.  Let's wait for
someone to complain they don't have /dev/stdin.