# HG changeset patch
# User haftmann
# Date 1281699835 -7200
# Node ID a461dd80f83c1754541ec3435caaade5fdcf26a9
# Parent  eccccdeb3f73ccaefa9b0129708ac980f955b494
ditem

diff -r eccccdeb3f73 -r a461dd80f83c doc-src/Codegen/style.sty
--- a/doc-src/Codegen/style.sty	Fri Aug 13 13:43:55 2010 +0200
+++ b/doc-src/Codegen/style.sty	Fri Aug 13 13:43:55 2010 +0200
@@ -15,6 +15,7 @@
 
 %% typographic conventions
 \newcommand{\qt}[1]{``{#1}''}
+\newcommand{\ditem}[1]{\item[\isastyletext #1]}
 
 %% verbatim text
 \newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}