Slightly more correct terminology on groups menu

diff --git a/lib/weblib.php b/lib/weblib.php
index bb018c0da8b59000506d40924231f60d1d59d30a..fac8d0eca69ae773e050a56a670f083ffe62f2e1 100644 (file)
--- a/lib/weblib.php
+++ b/lib/weblib.php
@@ -1687,7 +1687,7 @@ function print_group_menu($groups, $groupmode, $currentgroup, $urlroot) {
 /// Prints an appropriate group selection menu
 
 /// Add an "All groups" to the start of the menu
-    $groupsmenu[0] = get_string("allgroups");
+    $groupsmenu[0] = get_string("allparticipants");
     foreach ($groups as $key => $groupname) {
         $groupsmenu[$key] = $groupname;
     }