lib/Tools/mkdir
changeset 24450 70fd99d4ef82
parent 16482 ed08c8edc289
child 25172 ad25033f9ca4
--- a/lib/Tools/mkdir	Tue Aug 28 15:34:15 2007 +0200
+++ b/lib/Tools/mkdir	Tue Aug 28 16:33:52 2007 +0200
@@ -251,7 +251,7 @@
 
 \tableofcontents
 
-\parindent 0pt\parskip 0.5ex
+%\parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
 \input{session}