Merge pull request #49 from mtzguido/lax

Also use custom editor for .checked.lax files
FStarLang · Dec 27, 2024 · 8bf1768 · 8bf1768
2 parents be071b0 + a27064c
commit 8bf1768
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/package.json b/package.json
@@ -48,8 +48,14 @@
 					{
 						"filenamePattern": "*.fst.checked"
 					},
+					{
+						"filenamePattern": "*.fst.checked.lax"
+					},
 					{
 						"filenamePattern": "*.fsti.checked"
+					},
+					{
+						"filenamePattern": "*.fsti.checked.lax"
 					}
 				]
 			},