| changeset 27103 | d8549f4d900b |
| parent 25611 | c0deb7307732 |
| child 28142 | cf8da9bbc584 |
| 27102:a98cd7450204 | 27103:d8549f4d900b |
|---|---|
33 |
33 |
34 |
34 |
35 ## main |
35 ## main |
36 |
36 |
37 CMD=$(echo $CMD | sed -e 's/\\/\\\\"/g; s/"/\\\"/g') |
37 CMD=$(echo $CMD | sed -e 's/\\/\\\\"/g; s/"/\\\"/g') |
38 FULL_CMD="CodePackage.codegen_shell_command \"$THY\" \"$CMD\";" |
38 FULL_CMD="CodeTarget.shell_command \"$THY\" \"$CMD\";" |
39 |
39 |
40 "$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1 |
40 "$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1 |