diff --git a/languages.json b/languages.json index 4ff4b39c7..97f741966 100644 --- a/languages.json +++ b/languages.json @@ -578,7 +578,7 @@ "quotes": [["\\\"", "\\\""]], "line_comment": ["//"], "multi_line_comments": [["(*", "*)"]], - "extensions": ["fst"] + "extensions": ["fst", "fsti"] }, "Futhark": { "line_comment": ["--"],