diff --git a/repository/local/lib.php b/repository/local/lib.php
index 489156d4403..0dc7fac7076 100644
--- a/repository/local/lib.php
+++ b/repository/local/lib.php
@@ -132,11 +132,14 @@ class repository_local extends repository {
      * This function may skip subfolders and recursively add their children
      * {@link repository_local::can_skip()}
      *
-     * @param file_info $fileinfo
-     * @param string|array $extensions, for example '*' or array('.gif','.jpg')
+     * @param file_info|null $fileinfo
+     * @param string|string[] $extensions for example '*' or ['.gif', '.jpg']
      * @return array array of file_info elements
      */
-    private function get_non_empty_children(file_info $fileinfo, $extensions) {
+    private function get_non_empty_children(?file_info $fileinfo, $extensions): array {
+        if ($fileinfo === null) {
+            return [];
+        }
         $nonemptychildren = $fileinfo->get_non_empty_children($extensions);
         $list = array();
         foreach ($nonemptychildren as $child) {