function write_mhref(user, domain, text) {
    var at   = '@';
    var mail = user + at + domain;
    document.write("<a href='mailto:" + mail + "'>" + ( text == undefined ? mail : text ) + "</a>");
}