Consider gitignoring doc directory

[yunmikun2]

This git repository has generated documentation under version control which is unnecessary. They only take space while almost nobody, who wants to work on the project, needs to be stored in the repo. Also, it's a potential source of merge conflicts if these are to be commited by different people.