Skip to content

compress Json output to be on single line#144

Open
FrederickPu wants to merge 1 commit into
leanprover-community:masterfrom
FrederickPu:repl-compress-out
Open

compress Json output to be on single line#144
FrederickPu wants to merge 1 commit into
leanprover-community:masterfrom
FrederickPu:repl-compress-out

Commits

Commits on Feb 4, 2026