Commit Graph

3 Commits

Author SHA1 Message Date
Fangrui Song
4d76108d6b Delete file_consumer.* 2018-09-20 19:48:20 -07:00
Fangrui Song
763106c3d4 Simplify pipeline and fix race 2018-09-20 01:08:31 -07:00
Fangrui Song
c7a6c5cd12 Make $ccls/reload reset DB and reload cached index files
$ccls/reload is renamed from $ccls/freshenIndex

This is useful when DB (merged index) diverges from backing IndexFile.

Also fix a semantic highlighting bug.
2018-09-12 17:01:52 -07:00