Skip to content

Commit

Permalink
make "list of results" plural
Browse files Browse the repository at this point in the history
  • Loading branch information
christinerose authored Jul 29, 2024
1 parent b64e5a7 commit 183b732
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion doc/driver.mld
Original file line number Diff line number Diff line change
Expand Up @@ -807,7 +807,7 @@ let index_generate ?(ignore_output = false) occurrence_file =
We turn the JSON index into a JavaScript file. In order to never block the UI, this file will be used as a web worker by [odoc] to perform searches:

- The search query will be sent as a plain string to the web worker, using the standard mechanism of message passing.
- The web worker has to send back the result as a message to the main thread, containing the list of result. Each entry of this list must have the same form it had in the original JSON file.
- The web worker has to send back the result as a message to the main thread, containing the list of results. Each entry of this list must have the same form it had in the original JSON file.
- The file must be given to the [odoc-support] URI.

In this driver, we use the MiniSearch JavaScript library. For more involved applications, we could use [index.js] to call a server-side search engine via an API call.
Expand Down

0 comments on commit 183b732

Please sign in to comment.