Gut. Ich bin mir nicht sicher, ob 800 immer reicht, z.B. bei mehreren Suchausdrücken. Bei einem höheren Wert dauert es außerdem auch bei den anderen Suchmaschinen länger, bis die Hervorhebungen da sind. Darum meine ich, dass wir diese Änderungen noch nicht nach Github übernehmen, vielleicht findet sich da noch eine andere Lösung. Es sei denn, Mithrandir will es so.
Ich suche außerdem nach den Seiten mit den neuesten Versionen der Skripte von Griever.
Ich kenne bis jetzt nur: https://github.com/Griever/userChromeJS
Es muss aber noch etwas anderes geben, denn unser UserScriptLoader ist neuer als der auf Grievers Github-Site. Weiß jemand etwas dazu, insbes. woher unser UserScriptLoader stammt?