# HG changeset patch
# User wenzelm
# Date 1385208672 -3600
# Node ID 7fa522b213a8b40308b38c3691c07ca28f33e365
# Parent  301a721af68b1678af9acc3e92736e29786310db
more official option;

diff -r 301a721af68b -r 7fa522b213a8 src/Tools/Code/lib/Tools/codegen
--- a/src/Tools/Code/lib/Tools/codegen	Fri Nov 22 21:13:44 2013 +0100
+++ b/src/Tools/Code/lib/Tools/codegen	Sat Nov 23 13:11:12 2013 +0100
@@ -13,7 +13,7 @@
   echo "Usage: isabelle $PRG [OPTIONS] IMAGE THYNAME CMD"
   echo
   echo "  Options are:"
-  echo "    -q    run in quick'n'dirty mode"
+  echo "    -q    run in quick_and_dirty mode"
   echo
   echo "  Issues code generation using image IMAGE,"
   echo "  theory THYNAME,"