Skip to content

Commit 6227e5a

Browse files
fix: also move tutorials test file (#721)
The tutorials branch was from before the moving of test code, and thus had an old directory name when it got merged.
1 parent eec24f1 commit 6227e5a

File tree

7 files changed

+2
-2
lines changed

7 files changed

+2
-2
lines changed

lakefile.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -158,11 +158,11 @@ lean_exe simplepage where
158158

159159
@[default_target]
160160
lean_lib TutorialExample where
161-
srcDir := "examples/tutorial-examples"
161+
srcDir := "test-projects/tutorial-test"
162162

163163
@[default_target]
164164
lean_exe «tutorial-example» where
165-
srcDir := "examples/tutorial-examples"
165+
srcDir := "test-projects/tutorial-test"
166166
root := `Main
167167
supportInterpreter := true
168168

File renamed without changes.
File renamed without changes.

examples/tutorial-examples/TutorialExample/HashMap.lean renamed to test-projects/tutorial-test/TutorialExample/HashMap.lean

File renamed without changes.
File renamed without changes.

examples/tutorial-examples/TutorialExample/RCases.lean renamed to test-projects/tutorial-test/TutorialExample/RCases.lean

File renamed without changes.

0 commit comments

Comments
 (0)