Fix a notice buried in the HTML.

diff --git a/course/student.html b/course/student.html
index c8dec7562bf8af4458d3d24778263117bd9d3826..af6f16a9d41df7d82dc76967b519b9078c59e7c1 100644 (file)
--- a/course/student.html
+++ b/course/student.html
@@ -47,9 +47,11 @@
                   }
                   echo "</optgroup>\n";
               }
-              foreach ($users as $user) {
-                  $fullname = fullname($user, true);
-                  echo "<option value=\"$user->id\">".$fullname.", ".$user->email."</option>\n";
+              if (!empty($users)) {
+                  foreach ($users as $user) {
+                      $fullname = fullname($user, true);
+                      echo "<option value=\"$user->id\">".$fullname.", ".$user->email."</option>\n";
+                  }
               }
           ?>
          </select>