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}