WMDE-Fisch de99612520 Rename tag/user highlighting to free up the term ... While working on renaming and consolidating some methods I found it puzzeling, that the generic "highlight" word is already taken by the filter mechanism. So I made these things more specific. I checked the global wiki search if any user referes to these to override CSS. It seems nobody does, so the change should be save. Change-Id: I47c149978b0527c2d9e91709ef9d704526d56101		2023-09-05 12:01:02 +00:00
..
diff.page.js	Rename tag/user highlighting to free up the term	2023-09-05 12:01:02 +00:00