Add .lean, .lean4, and .hs as editable/viewable file types (#31716)

GitOrigin-RevId: c3ee7592d0a1096ac96ca9514579c559d028b840
This commit is contained in:
Copilot
2026-03-09 09:05:48 +00:00
committed by Copybot
parent 684bbe9186
commit 27aac33259
5 changed files with 15 additions and 0 deletions
+3
View File
@@ -74,6 +74,9 @@ function resetMeta() {
'gv',
'mf',
'lhs',
'lean',
'lean4',
'hs',
'mk',
'xmpdata',
'cfg',
+3
View File
@@ -60,6 +60,9 @@ const defaultTextExtensions = [
'yml',
'yaml',
'lhs',
'lean',
'lean4',
'hs',
'mk',
'xmpdata',
'cfg',
@@ -44,6 +44,9 @@ export function resetMeta() {
'gv',
'mf',
'lhs',
'lean',
'lean4',
'hs',
'mk',
'xmpdata',
'cfg',
@@ -129,6 +129,9 @@ describe('RestoreManager', function () {
'yml',
'yaml',
'lhs',
'lean',
'lean4',
'hs',
'mk',
'xmpdata',
'cfg',
@@ -138,6 +138,9 @@ describe('FileTypeManager', function () {
'/something/file.m',
'/file.TEX',
'/file.lhs',
'/file.lean',
'/file.lean4',
'/file.hs',
'/file.xmpdata',
'/file.cfg',
'/file.Rnw',