Fix linting.

FStarLang · Oct 15, 2024 · 95a58d0 · 95a58d0
1 parent 40b9b11
commit 95a58d0
Showing 1 changed file with 8 additions and 2 deletions.
diff --git a/eslint.config.mjs b/eslint.config.mjs
@@ -34,6 +34,12 @@ export default tseslint.config(
       '@typescript-eslint/no-unsafe-member-access': 0,
       '@typescript-eslint/no-unsafe-argument': 0,
       '@typescript-eslint/no-unsafe-call': 0,
-    },
-  }
+    }
+  },
+  {
+    ignores: [
+      "*/out/**",
+      "**/node_modules/**",
+    ]
+  },
 );