Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Github Issue #107: Deleted filesnames were not removed from the map o…
…f MkTextDocument. This meant MkTextDocument objects still existed when even their respective files were already deleted. Now those all those documents from the map are removed properly.
- Loading branch information