Testing moogle too

leanprover-community · Sep 13, 2024 · 3d42be7 · 3d42be7
1 parent 9bca41a
commit 3d42be7
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 0 deletions.
diff --git a/LeanSearchClientTest.lean b/LeanSearchClientTest.lean
@@ -1 +1,2 @@
 import LeanSearchClientTest.Examples
+import LeanSearchClientTest.MoogleExamples
diff --git a/LeanSearchClient/MoogleExamples.lean → LeanSearchClientTest/MoogleExamples.lean b/LeanSearchClient/MoogleExamples.lean → LeanSearchClientTest/MoogleExamples.lean
Original file line number	Diff line number	Diff line change
		@@ -1 +1,2 @@
		import LeanSearchClientTest.Examples
		import LeanSearchClientTest.MoogleExamples