From 263103153fd8782ff95c4d075339a445a64bea1d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 5 Oct 2010 15:27:56 +0000 Subject: [PATCH] =?utf8?q?=C3=82=C2=A3-=20use=20-----------=20in=20place?= =?utf8?q?=20of=20##=20for=20sequents?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit --- matita/components/content_pres/boxPp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matita/components/content_pres/boxPp.ml b/matita/components/content_pres/boxPp.ml index 0d58d9764..295275ee3 100644 --- a/matita/components/content_pres/boxPp.ml +++ b/matita/components/content_pres/boxPp.ml @@ -33,7 +33,7 @@ let string_space = " " let string_space_len = String.length string_space let string_indent = (* string_space *) "" let string_indent_len = String.length string_indent -let string_ink = "##" +let string_ink = "---------------------------" let string_ink_len = String.length string_ink let contains_attrs contained container = -- 2.39.2