Update lakefile.toml

2024-11-11 12:13:39 +00:00 · 2024-11-11 12:13:39 +00:00 · 278848247c
commit 278848247c
parent 3471e0d9ec
1 changed files with 1 additions and 0 deletions
--- a/lakefile.toml
+++ b/lakefile.toml
@ -58,6 +58,7 @@ srcDir = "scripts"

 [[lean_exe]]
 name = "stats"
+supportInterpreter = true
 srcDir = "scripts"

 [[lean_exe]]