Ticket #2383: delete.js

function delete_checked() {
    document.delete_checked_form.submit();
}