Function pushDecoder

Pagetual/pagetual.user.js:4205–4210

                }
            };
            let pushDecoder = label => {
                let raw = String(label || "").trim();
                if (raw && decoderList.indexOf(raw) === -1) {
                    decoderList.push(raw);
                }
            };
            let normalizedPreferred = normalize(preferredCharset).replace(/["']/g, "");
            pushDecoder(preferredCharset);
            pushDecoder(normalizedPreferred);