# Read a line from the standard input (`stdin`).
fun gets: String
do
	return sys.stdin.read_line
end