lib/Tools/codegen
changeset 27103 d8549f4d900b
parent 25611 c0deb7307732
child 28142 cf8da9bbc584
--- a/lib/Tools/codegen	Tue Jun 10 15:30:01 2008 +0200
+++ b/lib/Tools/codegen	Tue Jun 10 15:30:06 2008 +0200
@@ -35,6 +35,6 @@
 ## main
 
 CMD=$(echo $CMD | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
-FULL_CMD="CodePackage.codegen_shell_command \"$THY\" \"$CMD\";"
+FULL_CMD="CodeTarget.shell_command \"$THY\" \"$CMD\";"
 
 "$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1