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