../

How to switch between stdin and a file

if [[ "$#" -lt 1 ]]; then
	input_file="/dev/stdin"
else
	if [[ ! -f "$1" ]]; then
		echoerr "$PROGNAME: $1 doesn't exist"
		exit 1
	fi
	input_file="$1"
fi