Commented out non-standard paragraph formatting.
authornipkow
Tue, 28 Aug 2007 16:33:52 +0200
changeset 24450 70fd99d4ef82
parent 24449 2f05cb7fed85
child 24451 7c205d006719
Commented out non-standard paragraph formatting.
lib/Tools/mkdir
--- 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}