Merge pull request #1351 from duglin/fixtool

ignore .github files

Author: duglin

tools/verify.py

@@ -29,6 +29,7 @@
 _REPO_ROOT = _TOOLS_DIR.parent
 _FAKE_DOCS_DIR = Path(__file__).parent / "fake-docs"
 _FAKE_DOCS = set(_FAKE_DOCS_DIR.rglob("**/*"))
+_FAKE_DOCS.update(Path(".github").rglob("**/*"))
 _LANGUAGES_DIR_NAME = "languages"
 _ROOT_LANGUAGES_DIR = _REPO_ROOT / _LANGUAGES_DIR_NAME