From d9ff29a46bbf7453a9a75c81749e5568931a06d8 Mon Sep 17 00:00:00 2001
From: Jonas Jenwald <jonas.jenwald@gmail.com>
Date: Sun, 21 Jul 2024 19:26:15 +0200
Subject: [PATCH] Remove the unused `AppOptions.remove` method

This method has *never* been used anywhere in the code-base, so I really don't know why I added it originally.
---
 web/app_options.js | 14 +-------------
 1 file changed, 1 insertion(+), 13 deletions(-)

diff --git a/web/app_options.js b/web/app_options.js
index 7940d97863dd9..001fa72ddb14c 100644
--- a/web/app_options.js
+++ b/web/app_options.js
@@ -475,8 +475,7 @@ if (typeof PDFJSDev === "undefined" || PDFJSDev.test("GENERIC")) {
 const userOptions = new Map();
 
 if (typeof PDFJSDev === "undefined" || PDFJSDev.test("GENERIC")) {
-  // Apply any compatibility-values to the user-options,
-  // see also `AppOptions.remove` below.
+  // Apply any compatibility-values to the user-options.
   for (const [name, value] of compatParams) {
     userOptions.set(name, value);
   }
@@ -611,17 +610,6 @@ class AppOptions {
       }
     }
   }
-
-  static remove(name) {
-    userOptions.delete(name);
-
-    if (typeof PDFJSDev === "undefined" || PDFJSDev.test("GENERIC")) {
-      // Re-apply a compatibility-value, if it exists, to the user-options.
-      if (compatParams.has(name)) {
-        userOptions.set(name, compatParams.get(name));
-      }
-    }
-  }
 }
 
 if (typeof PDFJSDev === "undefined" || PDFJSDev.test("GENERIC")) {