From 2510808ebff2a51377a2c70b4f3be199158c6bba Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sun, 3 Mar 2024 21:19:17 +0100
Subject: [PATCH] chore: add unicode directory name to gitignore (#3565)

fixes #3358

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
---
 src/lake/tests/init/.gitignore | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/lake/tests/init/.gitignore b/src/lake/tests/init/.gitignore
index ecdd6a0190..22dc8beff0 100644
--- a/src/lake/tests/init/.gitignore
+++ b/src/lake/tests/init/.gitignore
@@ -5,6 +5,6 @@
 /hello-exe
 /lean-data
 /123-hello
-/«A.B».«C.D»
+/«A-B»-«C-D»
 /meta
 /qed