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