From b00d9575f8f448fdb689217419caa3d788f507e8 Mon Sep 17 00:00:00 2001
From: Rob Garrison <wowmotty@gmail.com>
Date: Sat, 26 Aug 2017 10:29:33 -0500
Subject: [PATCH] Clear linter config history

---
 edit/lint.js | 1 +
 1 file changed, 1 insertion(+)

diff --git a/edit/lint.js b/edit/lint.js
index 8f1e3c5f..a6d90e50 100644
--- a/edit/lint.js
+++ b/edit/lint.js
@@ -392,6 +392,7 @@ function setupLinterPopup(rules) {
   contents.insertBefore(popup.codebox.display.wrapper, contents.firstElementChild);
   popup.codebox.focus();
   popup.codebox.setValue(rules);
+  popup.codebox.clearHistory();
   onDOMscripted(loadJSON).then(() => setJSONMode(popup.codebox));
   setupLinterSettingsEvents(popup);
 }