"error: type must be string, but is null"

[rgrinberg]

I get this error:

error: type must be string, but is null [3 times]

it seems like lean insists on sending buffer file names that are null:

16:54:28.640 -- server<= {"seq_num":150,"command":"roi","mode":"visible-lines-and-above","files":[{"file_name":"/Users/rgrinberg/tmp/lean/foo.lean","ranges":[{"begin_line":1,"end_line":15},{"begin_line":1,"end_line":15}]},{"file_name":"/Users/rgrinberg/reps/tmp/lean/pnotp.lean","ranges":null}]}
16:54:28.644 -- server<= {"seq_num":151,"command":"roi","mode":"visible-lines-and-above","files":[{"file_name":"/Users/rgrinberg/tmp/lean/foo.lean","ranges":[{"begin_line":1,"end_line":15},{"begin_line":1,"end_line":15}]},{"file_name":"/Users/rgrinberg/reps/tmp/lean/pnotp.lean","ranges":null}]}
16:54:28.674 -- server<= {"seq_num":152,"command":"roi","mode":"visible-lines-and-above","files":[{"file_name":null,"ranges":[{"begin_line":1,"end_line":6}]},{"file_name":"/Users/rgrinberg/tmp/lean/foo.lean","ranges":[{"begin_line":1,"end_line":15}]},{"file_name":"/Users/rgrinberg/reps/tmp/lean/pnotp.lean","ranges":null}]}
16:54:28.675 -- server<= {"seq_num":153,"command":"sync","file_name":null,"content":""}
16:54:28.675 -- server<= {"seq_num":154,"command":"info","file_name":null,"line":1,"column":0}
16:54:28.694 -- server=> {"response":"ok","seq_num":150}

It's probably not a problem, but it's annoying to see this spam in *messages*.