kframework/k — pull request #913 by osa1 (2014-08-31 13:51:05+00:00)
Title: --dry should not print commands with output redirections by default (see details inside)

ktest's `--dry` was generating commands with `... > output_file` parts. That was wrong because ktest generates output files only when `--generate-out` or `--update-out` arguments are provided.

(Also discussed at #892)

With this patch, `--dry` only generates `... > output_file` parts when `--generate-out` and `--update-out` are provided, and printed paths are same as what ktest would use when that arguments are used.

@daejunpark Small patch but I still don't understand `--generate-out` in all details so it'd be nice if you could review.