Skip to content

Commit 9b92234

Browse files
committed
Test new bench target on PR
1 parent 5a0e92c commit 9b92234

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

lakefile.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ lean_lib «Template» where
1313
lean_exe "template" where
1414
root := `Main
1515

16-
lean_exe "bench-test" where
16+
lean_exe "bench-test-new" where
1717
root := `Benchmarks.Main
1818

1919
script "get-exe-targets" := do

0 commit comments

Comments
 (0)