Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Remove unintentionally duplicated docs directory
This actually has the potential to mightily confused people on case-insensitive filesystems where this file can overwrite its sibling in /Doc/.
- Loading branch information