# Open the next file until there is no more arguments
	private fun open_next_stream
	do
		if args.is_empty then exit(0)
		stdin.close
		stdin = new FileReader.open(args.shift)
	end