From 09e24ce238319e26790fee36a8603be931255029 Mon Sep 17 00:00:00 2001
From: jos <wjosdejong@gmail.com>
Date: Wed, 28 Aug 2019 10:55:07 +0200
Subject: [PATCH] remove arrow function

---
 src/js/util.js | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/js/util.js b/src/js/util.js
index a825b31..45ad60b 100644
--- a/src/js/util.js
+++ b/src/js/util.js
@@ -1163,10 +1163,12 @@ exports.getPositionForPath = function(text, paths) {
  */
 exports.compileJSONPointer = function (path) {
   return path
-      .map(p => ('/' + String(p)
-          .replace(/~/g, '~0')
-          .replace(/\//g, '~1')
-      ))
+      .map(function (p) {
+        return ('/' + String(p)
+                .replace(/~/g, '~0')
+                .replace(/\//g, '~1')
+        );
+      })
       .join('');
 };