From e4135ce35de2b264d7560b37ca2344f6f206db59 Mon Sep 17 00:00:00 2001
From: eight <eight04@gmail.com>
Date: Fri, 28 Sep 2018 11:57:34 +0800
Subject: [PATCH] Fix: remove unused function

---
 js/prefs.js | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/js/prefs.js b/js/prefs.js
index e92f28dd..638b79eb 100644
--- a/js/prefs.js
+++ b/js/prefs.js
@@ -354,14 +354,6 @@ var prefs = new function Prefs() {
     if (Number(storage['editor.lintReportDelay']) === 4500) delete storage['editor.lintReportDelay'];
   }
 
-  function defineReadonlyProperty(obj, key, value) {
-    const copy = deepCopy(value);
-    if (typeof copy === 'object') {
-      Object.freeze(copy);
-    }
-    Object.defineProperty(obj, key, {value: copy, configurable: true});
-  }
-
   function equal(a, b) {
     if (!a || !b || typeof a !== 'object' || typeof b !== 'object') {
       return a === b;