From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 4 Sep 2006 14:22:34 +0000 (+0000)
Subject: no-indent
X-Git-Tag: 0.4.95@7852~1084
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8f34d1d64451220aba4de24cf322bdd826ff7248;p=helm.git

no-indent
---

diff --git a/components/content_pres/boxPp.ml b/components/content_pres/boxPp.ml
index 2957a3975..53149877e 100644
--- a/components/content_pres/boxPp.ml
+++ b/components/content_pres/boxPp.ml
@@ -31,7 +31,7 @@ module Pres = Mpresentation
 
 let string_space = " "
 let string_space_len = String.length string_space
-let string_indent = string_space
+let string_indent = (* string_space *) ""
 let string_indent_len = String.length string_indent
 let string_ink = "##"
 let string_ink_len = String.length string_ink