Damir Jelić 0c3d507455 EventIndex: Cancel the crawler early after a message request. ...

If we're cancelling the crawler nowadays this means that we're likely
deleting the index. Processing these messages is wasted effort in that
case so break early.

2020-01-24 11:46:46 +01:00

..

BaseEventIndexManager.js

EventIndexPanel: Get more stats for our indexer, not just the size.

2020-01-20 17:42:24 +01:00

EventIndex.js

EventIndex: Cancel the crawler early after a message request.

2020-01-24 11:46:46 +01:00

EventIndexPeg.js

EventIndexPeg: Style fix for a docstring.

2020-01-24 11:16:49 +01:00