removed debug logInfo

leanprover-community · Sep 19, 2024 · 3d5dbb0 · 3d5dbb0
1 parent 37d189f
commit 3d5dbb0
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/LeanSearchClient/LoogleSyntax.lean b/LeanSearchClient/LoogleSyntax.lean
@@ -148,7 +148,6 @@ syntax (name := loogle_cmd) "#loogle" loogle_filters  : command
   match stx with
   | `(command| #loogle $args:loogle_filters) =>
     let s := (← PrettyPrinter.ppCategory ``loogle_filters args).pretty
-    logInfo s
     let result ← getLoogleQueryJson s
     match result with
     | LoogleResult.success xs =>