# HG changeset patch
# User haftmann
# Date 1220590220 -7200
# Node ID cf8da9bbc58413f02771cef7652d06bd8aa0800a
# Parent  193c3ea0f63bc2806a32e10b0346f212a2a2ab94
renamed structure CodeTarget to Code_Target

diff -r 193c3ea0f63b -r cf8da9bbc584 lib/Tools/codegen
--- a/lib/Tools/codegen	Fri Sep 05 00:19:50 2008 +0200
+++ b/lib/Tools/codegen	Fri Sep 05 06:50:20 2008 +0200
@@ -35,6 +35,6 @@
 ## main
 
 CMD=$(echo $CMD | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
-FULL_CMD="CodeTarget.shell_command \"$THY\" \"$CMD\";"
+FULL_CMD="Code_Target.shell_command \"$THY\" \"$CMD\";"
 
 "$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1