If the uploaded file is HTML, then put it through the filters

diff --git a/file.php b/file.php
index 97052b04e16fbdc490e9fdf72eda5776ad776f97..6319b4407507809cefbdec18e527e15d33ecaf74 100644 (file)
--- a/file.php
+++ b/file.php
@@ -49,7 +49,12 @@
         header("Content-disposition: inline; filename=$filename");
         header("Content-length: ".filesize($pathname));
         header("Content-type: $mimetype");
-        readfile("$pathname");
+
+        if ($mimetype == "text/html") {
+            echo format_text(implode('', file($pathname)), FORMAT_HTML);  // Filter HTML files
+        } else {
+            readfile("$pathname");
+        }
     } else {
         error("Sorry, but the file you are looking for was not found ($pathname)", "course/view.php?id=$courseid");
     }