The search functionality needs JavaScript enabled
Changes the terminal's title
void setTitle ( string t );