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);