try breaking it first

leanprover · Jun 20, 2024 · 945d56a · 945d56a
1 parent ef3d5be
commit 945d56a
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 0 deletions.
diff --git a/tests/pkg/path with spaces/.gitignore b/tests/pkg/path with spaces/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/tests/pkg/path with spaces/Main.lean b/tests/pkg/path with spaces/Main.lean
@@ -0,0 +1,2 @@
+def main : IO Unit :=
+  IO.println s!"Hello, world!"
diff --git a/tests/pkg/path with spaces/lakefile.toml b/tests/pkg/path with spaces/lakefile.toml
@@ -0,0 +1,6 @@
+name = "path with spaces"
+defaultTargets = ["«path with spaces»"]
+
+[[lean_exe]]
+name = "path with spaces"
+root = "Main"
diff --git a/tests/pkg/path with spaces/test.sh b/tests/pkg/path with spaces/test.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+rm -rf .lake/build
+lake exe "«path with spaces»"
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		def main : IO Unit :=
		IO.println s!"Hello, world!"