Index: tools/copy_dart.py |
diff --git a/tools/copy_dart.py b/tools/copy_dart.py |
index 4230d52c66ab02d3f47ab3fb4cf6320bc93da2b0..1fd52a0067c973fea4dc3dfb3e6ee31be1964e4e 100755 |
--- a/tools/copy_dart.py |
+++ b/tools/copy_dart.py |
@@ -65,13 +65,6 @@ def mergefiles(srcs, dstfile): |
if not line.startswith('part of '): |
dstfile.write(line) |
-def copyfile(src, dst): |
- if not exists(dirname(dst)): |
- os.makedirs(dirname(dst)) |
- with open(src, 'r') as s: |
- with open(dst, 'w') as d: |
- d.write(s.read()) |
- |
def main(outdir = None, *inputs): |
if not outdir or not inputs: |
print "Usage: %s OUTDIR INPUTS" % args[0] |