idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-15 14:23:32 +03:00
Code Issues Projects Releases Wiki Activity

[ perf ] do not public export FromString

Browse Source
This commit is contained in:
Guillaume Allais 2022-03-07 12:18:39 +00:00 committed by G. Allais
parent c2718684d8
commit b87d7e3b62
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr
View File

@ -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