max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add unicode directory name to gitignore (#3565)

Browse source 
fixes #3358

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
This commit is contained in:
Joachim Breitner 2024-03-03 21:19:17 +01:00 • committed by GitHub
parent 9f305fb31f
commit 2510808ebf
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/lake/tests/init/.gitignore vendored
View file

@ -5,6 +5,6 @@
/hello-exe
/lean-data
/123-hello
/«A.B».«C.D»
/«A-B»-«C-D»
/meta
/qed