From 3d5dbb01d9a72ea885f39481cfa119a250e74372 Mon Sep 17 00:00:00 2001 From: Siddhartha Gadgil Date: Thu, 19 Sep 2024 07:00:57 +0530 Subject: [PATCH] removed debug logInfo --- LeanSearchClient/LoogleSyntax.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/LeanSearchClient/LoogleSyntax.lean b/LeanSearchClient/LoogleSyntax.lean index f11134b..93518ef 100644 --- 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 =>