make sure prefix of spaces path exists

leanprover · Jul 24, 2024 · 78d0819 · 78d0819
1 parent 632030a
commit 78d0819
Show file tree

Hide file tree

Showing 5 changed files with 1 addition and 0 deletions.
diff --git a/tests/pkg/path b/tests/pkg/path
@@ -0,0 +1 @@
+This file exists to check that its presence does not break the 'path with spaces' test on Windows
diff --git a/tests/pkg/spaces/.gitignore → tests/pkg/path with spaces/.gitignore b/tests/pkg/spaces/.gitignore → tests/pkg/path with spaces/.gitignore
diff --git a/tests/pkg/spaces/Main.lean → tests/pkg/path with spaces/Main.lean b/tests/pkg/spaces/Main.lean → tests/pkg/path with spaces/Main.lean
diff --git a/tests/pkg/spaces/lakefile.toml → tests/pkg/path with spaces/lakefile.toml b/tests/pkg/spaces/lakefile.toml → tests/pkg/path with spaces/lakefile.toml
diff --git a/tests/pkg/spaces/test.sh → tests/pkg/path with spaces/test.sh b/tests/pkg/spaces/test.sh → tests/pkg/path with spaces/test.sh
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		This file exists to check that its presence does not break the 'path with spaces' test on Windows