kframework/k — pull request #967 by daejunpark (2014-09-19 21:25:33+00:00)
Title: Add a built-in IO operator, #external, for executing an external process.

I've added a new built-in IO operator, `#external`. The usage is as follows.
@dwightguth @yilongli @andreistefanescu, please review.

Usage: The `#external` takes a string of command as an input and returns the
string of stdout. The command string should use `"\x01"` as a seperator instead
of whitespaces. For example, the following term:
```
#external("echo" +String "\x01" +String "ok!")
```
rewrites to `"ok!"`.