Daniel Hofmann 3e479d772b Closes #8123: Fix plus-handling (+) in search terms for basic html theme search ... Note, that the default splitter will not index +, so this isn't of much of much use, unless the splitter of the search-language is reconfigured.		2020-08-19 18:01:27 +02:00
..
doctools.js	Closes #8123: Fix plus-handling (+) in search terms for basic html theme search	2020-08-19 18:01:27 +02:00
searchtools.js	Closes #8123: Fix plus-handling (+) in search terms for basic html theme search	2020-08-19 18:01:27 +02:00