Merge cf8b54d020 into 84c6914a9b

Merge pull request #4828 from quantum9Innovation/lean-gitignore
feat: create Lean.gitignore
2026-08-30 11:47:22 +02:00 · 2026-04-04 06:01:06 +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 14 additions and 4 deletions
--- a/Agda.gitignore
+++ b/Agda.gitignore
@ -1,2 +1,2 @@
 *.agdai
-MAlonzo/**
+**/MAlonzo/**
--- a/Global/VirtualEnv.gitignore
+++ b/Global/VirtualEnv.gitignore
@ -1,5 +1,16 @@
 # Virtualenv
 # https://realpython.com/python-virtual-environments-a-primer/#the-virtualenv-project
 .venv/
 venv/
 .python-version
 # pyenv: Simple Python Version Management
 pyvenv.cfg
 # pip: package installer for Python
 pip-selfcheck.json
 # Custom python interpreter
 .Python
 [Bb]in
 [Ii]nclude
@ -7,6 +18,3 @@
 [Ll]ib64
 [Ll]ocal
 [Ss]cripts
 pyvenv.cfg
 .venv
 pip-selfcheck.json
--- a/Lean.gitignore
+++ b/Lean.gitignore
@ -0,0 +1,2 @@
 # cache and other artifacts produced by Lean's Lake build tool
 .lake/
Author	SHA1	Message	Date
Luís Pedro Algarvio	a0185d1ea9	Merge `cf8b54d020` into `84c6914a9b`	2026-04-04 06:01:06 +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 Venkatesh	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
Luís Pedro Algarvio	cf8b54d020	Update VirtualEnv.gitignore	2025-08-21 02:51:00 +01:00
Luís Pedro Algarvio	add7cbcaad	Update VirtualEnv.gitignore Add extra rules	2025-08-21 02:33:54 +01:00
`@ -1,2 +1,2 @@`
	`*.agdai`	`*.agdai`
	`MAlonzo/**`	`/MAlonzo/`
		`@ -0,0 +1,2 @@`
							`# cache and other artifacts produced by Lean's Lake build tool`
							`.lake/`