summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--application/models/mfile.php3
1 files changed, 3 insertions, 0 deletions
diff --git a/application/models/mfile.php b/application/models/mfile.php
index 0a97da5a6..e32ea6bf4 100644
--- a/application/models/mfile.php
+++ b/application/models/mfile.php
@@ -360,7 +360,10 @@ class Mfile extends CI_Model {
$extension = substr($name, strrpos($name, ".") + 1);
$extensionarray = array(
+ 'mli' => 'ocaml',
+ 'mll' => 'ocaml',
'ml' => 'ocaml',
+ 'mly' => 'ocaml',
'tcl' => 'tcl',
'tex' => 'tex',
);