| 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] | 
|  |