| changeset 28502 | 6b0e3e4e1891 |
| parent 28142 | cf8da9bbc584 |
| child 28650 | a7ba12e0d3b7 |
| 28501:4a6c9881adc0 | 28502:6b0e3e4e1891 |
|---|---|
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="Code_Target.shell_command \"$THY\" \"$CMD\";" |
38 FULL_CMD="Code_Target.shell_command \"$THY\" \"$CMD\";" |
39 |
39 |
40 "$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1 |
40 "$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1 |