renamed structure CodeTarget to Code_Target
authorhaftmann
Fri, 05 Sep 2008 06:50:20 +0200
changeset 28142 cf8da9bbc584
parent 28141 193c3ea0f63b
child 28143 e5c6c4aac52c
renamed structure CodeTarget to Code_Target
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