lib/Tools/codegen
changeset 28142 cf8da9bbc584
parent 27103 d8549f4d900b
child 28502 6b0e3e4e1891
--- 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