]> matita.cs.unibo.it Git - helm.git/commitdiff
no-indent
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 4 Sep 2006 14:22:34 +0000 (14:22 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 4 Sep 2006 14:22:34 +0000 (14:22 +0000)
components/content_pres/boxPp.ml

index 2957a3975446f48c3c0c69e763d3ba45eccd43cc..53149877ea73a1eb71e3c5b2f75ec4f7f78df552 100644 (file)
@@ -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