diff --git a/tools/Examples.py b/tools/Examples.py
index fa81e245..9126427e 100644
--- a/tools/Examples.py
+++ b/tools/Examples.py
@@ -26,11 +26,9 @@ startBuild = """\
-
"""
endBuild = """\
-
@@ -166,11 +164,12 @@ def destDirs(pattern="**"):
def copySupplementalFilesFromGithub():
- for common in githubDirs().intersection(destDirs()):
- print("->", common)
- build = github / common / "build.xml"
- target = destination / common
- shutil.copy(str(build), str(target))
+ # for common in githubDirs().intersection(destDirs()):
+ # print("->", common)
+ # build = github / common / "build.xml"
+ # target = destination / common
+ # shutil.copy(str(build), str(target))
+ shutil.copy(str(github / "build.xml"), str(destination))
shutil.copy(str(github / "Ant-Common.xml"), str(destination))
for face in (github / "gui").glob("*.gif"):
shutil.copy(str(face), str(destination / "gui"))