# HG changeset patch
# User nipkow
# Date 1220981602 -7200
# Node ID 3f69c3c5447832c6c89a60bfdc09d680efd6c296
# Parent  8e8313aededc07eecf1dcb02f1951e60bf006c90
added comment

diff -r 8e8313aededc -r 3f69c3c54478 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}