diff --git a/repository/lib.php b/repository/lib.php index 353f6b14829..39f6b92bee2 100644 --- a/repository/lib.php +++ b/repository/lib.php @@ -1938,7 +1938,7 @@ EOD; $accepted_file_ext = json_encode($ft->get_file_ext($accepted_filetypes)); $js .= << + @@ -1959,7 +1959,7 @@ EOD; // print repository instances listing $js .= << +