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