micbou ee25d5b8eb Close options file before starting server ... On Windows, the options file cannot be deleted while it is still open by another process. Close the file before starting the server. Do not explicitly flush the file as closing implies flushing.		2017-09-23 14:13:02 +02:00
..
ycm	Close options file before starting server	2017-09-23 14:13:02 +02:00
test_requirements.txt	Require coverage.py older than 4.4	2017-06-04 16:42:54 +02:00