Role names are not multilang-filtered on course user list

In /user/index.php, the role names in the string "Users with the role x" do not get filtered so that the multilang filter does not get applied to this string.

In v. 1.142.2.11, line 428 needs to be changed from:
print_heading($heading, 'center', 3);
to:
print_heading(format_string($heading), 'center', 3);