Use '/' key to quickly access this field.
Enter name of repository, or repository group for quick search.
Prefix query to allow special search:
user:admin, to search for usernames
user_group:devops, to search for user groups
commit:efced4, to search for commits
$("body").prepend("<div class=\"alert alert-info\"> Submission #{@submission.id}'s task status has been changed to \"#{@task.status_str}\". It will be re-judged soon. </div>")