1 function delete_cookie ( cookie_name )
3 var cookie_date = new Date ( );
4 cookie_date.setTime ( cookie_date.getTime() - 1 );
5 document.cookie = cookie_name += "=; expires=" + cookie_date.toGMTString();
10 delete_cookie(document.cookie);
12 document.cookie="username="+ document.getElementById('username').value;
13 document.cookie="password=" + document.getElementById('password').value;
14 window.location = 'index.php';
15 //alert(document.cookie);
20 delete_cookie(document.cookie);
21 window.location = 'index.php';
24 function line_comment(line_com, line_input)
26 // unhide div at this line
27 document.getElementById(line_com).style.display = "block";
29 document.getElementById(line_input).focus();
32 function line_comment_cancel(line_com)
34 document.getElementById(line_com).style.display = "none";
37 function line_comment_save(file_id, line_num, page_element, comment)
39 // verify payload not empty
40 if(document.getElementById(comment).value == "") { return; }
41 getPage("line_comment.php?file_id="+file_id+"&line_num="+line_num+"&comment=\""+document.getElementById(comment).value+"\"", page_element, "Please Wait")
44 function line_comment_refresh(page_element)
46 //alert("Changing block" + document.getElementById(page_element).value);
47 //document.getElementById(page_element).innerHTML = "Boo";