$name .= ' <a href="https://www.polytechnique.org/marketing/broken/' . $user->hruid . '"><img src="images/icons/error.gif" alt="Patte cassée" /></a>';
}
if ($with_groupperms && $user instanceof User && $user->group_perms == 'admin' && !empty($name)) {
$name .= ' <a href="https://www.polytechnique.org/marketing/broken/' . $user->hruid . '"><img src="images/icons/error.gif" alt="Patte cassée" /></a>';
}
if ($with_groupperms && $user instanceof User && $user->group_perms == 'admin' && !empty($name)) {