Merge 6d24007ad2 into 84c6914a9b

Merge pull request #4828 from quantum9Innovation/lean-gitignore
feat: create Lean.gitignore
2026-11-05 09:34:38 +01:00 · 2026-04-04 04:14:51 +00:00 · 2026-04-03 17:05:51 -07:00 · 2026-04-03 20:04:27 -04:00 · 2026-04-03 14:15:11 -07:00 · 2026-03-28 21:42:41 -07:00
3 changed files with 4 additions and 7 deletions
@@ -1,2 +1,2 @@
 *.agdai
-MAlonzo/**
+**/MAlonzo/**
@@ -0,0 +1,2 @@
+# cache and other artifacts produced by Lean's Lake build tool
+.lake/
@@ -407,12 +407,7 @@ MigrationBackup/
 FodyWeavers.xsd

 # VS Code files for those working on multiple tools
-.vscode/*
-!.vscode/settings.json
-!.vscode/tasks.json
-!.vscode/launch.json
-!.vscode/extensions.json
-!.vscode/*.code-snippets
+!.vscode/*

 # Local History for Visual Studio Code
 .history/
Author	SHA1	Message	Date
Benjamin Michaelis	3e35dc690c	Merge `6d24007ad2` into `84c6914a9b`	2026-04-04 04:14:51 +00:00
Devin Dooley	84c6914a9b	Merge pull request #4828 from quantum9Innovation/lean-gitignore feat: create Lean.gitignore	2026-04-03 17:05:51 -07:00
Ananth VenkateshandDevin Dooley	5f760225cf	fix: only match on `.lake` directory Co-authored-by: Devin Dooley <dooleydevin@github.com>	2026-04-03 20:04:27 -04:00
Devin Dooley	f963896e65	Merge pull request #4818 from vicgeentor/patch-1 Update Agda.gitignore to exclude MAlonzo directories in any location	2026-04-03 14:15:11 -07:00
Ananth Venkatesh	b9ad512a45	feat: create Lean.gitignore	2026-03-28 21:42:41 -07:00
Vic	8431b56bed	include MAlonzo directories in any location	2026-03-18 14:07:30 +01:00
Benjamin Michaelis	6d24007ad2	Update VisualStudio.gitignore to include all VS Code files	2025-10-01 14:23:00 -07:00
Benjamin Michaelis	2b90570de6	feat: Add mcp.json to Visual Studio gitignore exceptions As mcp's are becoming more common, sharing a workspace configuration of mcp servers is becoming more and more common with the mcp.json file. (https://code.visualstudio.com/docs/copilot/customization/mcp-servers#_add-an-mcp-server) Adding this file as an exclusion to the default template so that it can be utilized by the editors and shared via source control. This file can also be picked up by Visual Studio as seen [here](https://learn.microsoft.com/visualstudio/ide/mcp-servers?view=vs-2022&WT.mc_id=8B97120A00B57354#file-locations-for-automatic-discovery-of-mcp-configuration)	2025-09-23 11:14:46 -07:00