chore: Remove tomograph as default target

2025-07-11 16:27:14 -07:00 · 2025-07-11 16:27:14 -07:00 · 147d3cc87e
parent 752d13182d
commit 147d3cc87e
1 changed files with 0 additions and 1 deletions
--- a/lakefile.lean
+++ b/lakefile.lean
@ -18,7 +18,6 @@ lean_exe repl {
  supportInterpreter := true
 }

-@[default_target]
 lean_exe tomograph {
  root := `Tomograph
  -- Solves the native symbol not found problem