function set_title(t) {
    document.title = t;
}