diff options
| author | Joel Martin <github@martintribe.org> | 2015-03-02 21:33:10 -0600 |
|---|---|---|
| committer | Joel Martin <github@martintribe.org> | 2015-03-02 21:33:10 -0600 |
| commit | 835fb7d8b06e2b44792a97ac89994658bf6d00af (patch) | |
| tree | 578f67726ab9e3ce5fcbc50220e9761a66c5ddf1 /php/printer.php | |
| parent | 6b72e6078a7d505ecf9d711eb4a16fc4dfac36b6 (diff) | |
| parent | 8a98ef9a3f3a6b6d05d02dc305a0c886c907e0f3 (diff) | |
| download | mal-835fb7d8b06e2b44792a97ac89994658bf6d00af.tar.gz mal-835fb7d8b06e2b44792a97ac89994658bf6d00af.zip | |
Merge branch 'master' into gh-pages
Conflicts:
.gitignore
Diffstat (limited to 'php/printer.php')
| -rw-r--r-- | php/printer.php | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/php/printer.php b/php/printer.php index 3839931..130d31b 100644 --- a/php/printer.php +++ b/php/printer.php @@ -23,7 +23,9 @@ function _pr_str($obj, $print_readably=True) { } return "{" . implode(" ", $ret) . "}"; } elseif (is_string($obj)) { - if ($print_readably) { + if (strpos($obj, chr(0x7f)) === 0) { + return ":".substr($obj,1); + } elseif ($print_readably) { $obj = preg_replace('/"/', '\\"', preg_replace('/\\\\/', '\\\\\\\\', $obj)); return '"' . $obj . '"'; } else { |