added comment
authornipkow
Tue, 09 Sep 2008 19:33:22 +0200
changeset 28180 3f69c3c54478
parent 28179 8e8313aededc
child 28181 e98be9824b7d
added comment
lib/Tools/mkdir
--- a/lib/Tools/mkdir	Tue Sep 09 16:59:48 2008 +0200
+++ b/lib/Tools/mkdir	Tue Sep 09 19:33:22 2008 +0200
@@ -242,6 +242,9 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
 
 \begin{document}