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