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