From 50c6a3ac9ff4675f83476c3e48fa916949df35e6 Mon Sep 17 00:00:00 2001
From: jos <wjosdejong@gmail.com>
Date: Thu, 28 Dec 2017 16:18:46 +0100
Subject: [PATCH] Updated history

---
 HISTORY.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/HISTORY.md b/HISTORY.md
index 3cb628b..8b1c392 100644
--- a/HISTORY.md
+++ b/HISTORY.md
@@ -3,6 +3,12 @@
 https://github.com/josdejong/jsoneditor
 
 
+## not yet released, version 5.13.1
+
+- Fixed another occurrence of #494: properties not escaped in the
+  navigation bar.
+
+
 ## 2017-12-28, version 5.13.0
 
 - Implemented cursor position in text mode. Thanks @meirotstein.