From 46cd2c18958d6e169b65ddd5f670a9b2cbaf6296 Mon Sep 17 00:00:00 2001
From: Jason Davies <jason@jasondavies.com>
Date: Tue, 8 Oct 2013 14:20:55 +0100
Subject: [PATCH] Better escaping of null characters.

If a null character isn't followed by a digit, then it should be safe to
escape it using the shorter sequence "\0" instead of "\x00".
---
 lib/output.js | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/lib/output.js b/lib/output.js
index e7f3f4dd..a29e6969 100644
--- a/lib/output.js
+++ b/lib/output.js
@@ -84,7 +84,7 @@ function OutputStream(options) {
 
     function make_string(str) {
         var dq = 0, sq = 0;
-        str = str.replace(/[\\\b\f\n\r\t\x22\x27\u2028\u2029\0]/g, function(s){
+        str = str.replace(/[\\\b\f\n\r\t\x22\x27\u2028\u2029\0]/g, function(s, i){
             switch (s) {
               case "\\": return "\\\\";
               case "\b": return "\\b";
@@ -95,7 +95,9 @@ function OutputStream(options) {
               case "\u2029": return "\\u2029";
               case '"': ++dq; return '"';
               case "'": ++sq; return "'";
-              case "\0": return "\\x00";
+              case "\0":
+                var next = s.charCodeAt(i + 1);
+                return 48 <= next && next <= 57 ? "\\x00" : "\\0";
             }
             return s;
         });