diff options
Diffstat (limited to 'application/models/mfile.php')
| -rw-r--r-- | application/models/mfile.php | 3 |
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', ); |