From a3de78419b8cd9d07833e209b406e76b57d545ad Mon Sep 17 00:00:00 2001
From: Gilgamesh Athoraya <e9gille@gmail.com>
Date: Wed, 20 Jun 2018 16:03:15 +0200
Subject: [PATCH] change label for show editor toolbar pref, fix #462

---
 index.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/index.html b/index.html
index d32ee0b1..b43fd424 100644
--- a/index.html
+++ b/index.html
@@ -521,7 +521,7 @@ <h2>Minimap</h2>
       <hr>
       <h2>Other</h2>
       <p><label class=cb_label><input id=code_sqp   type=checkbox>Show <u>q</u>uit prompt</label></p>
-      <p><label class=cb_label><input id=code_set   type=checkbox>Show editor toolbar</label></p>
+      <p><label class=cb_label><input id=code_set   type=checkbox>Show toolbar in editor/trace windows</label></p>
       <p><label class=cb_label><input id=code_coq  type=checkbox>Connect on quit</label></p>
     </div>