From 147d3cc87e0bf85720be22dde203d991f398d434 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 11 Jul 2025 16:27:14 -0700
Subject: [PATCH] chore: Remove tomograph as default target

---
 lakefile.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/lakefile.lean b/lakefile.lean
index 194fbfc..8ab791f 100644
--- 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