From b87d7e3b62e0cf5f31f792eff67ed161e647566c Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Mon, 7 Mar 2022 12:18:39 +0000 Subject: [PATCH] [ perf ] do not public export FromString --- src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr b/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr index e9f8057d8..17a119907 100644 --- a/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr +++ b/src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr @@ -364,7 +364,7 @@ Pretty String where pretty str = let str' = if "\n" `isSuffixOf` str then dropLast 1 str else str in vsep $ map unsafeTextWithoutNewLines $ lines str' -public export +export FromString (Doc ann) where fromString = pretty