Index: tools/make_links.py |
diff --git a/tools/make_links.py b/tools/make_links.py |
index 157008ace7b4944644e8e4064747afafdaf01602..f49c0ed1a36f2a8a20b2bc8c03bd95a9bffc6af6 100644 |
--- a/tools/make_links.py |
+++ b/tools/make_links.py |
@@ -42,24 +42,15 @@ def get_options(): |
def make_link(source, target, orig_source): |
if os.path.islink(target): |
- print 'Removing %s' % target |
- sys.stdout.flush() |
os.unlink(target) |
if os.path.isdir(target): |
- print 'Removing %s' % target |
- sys.stdout.flush() |
os.rmdir(target) |
if os.path.isfile(orig_source): |
- print 'Copying file from %s to %s' % (orig_source, target) |
- sys.stdout.flush() |
shutil.copyfile(orig_source, target) |
return 0 |
else: |
- print 'Creating link from %s to %s' % (source, target) |
- sys.stdout.flush() |
- |
if utils.GuessOS() == 'win32': |
return subprocess.call(['mklink', '/j', target, source], shell=True) |
else: |
@@ -90,7 +81,7 @@ def main(argv): |
os.remove(full_link) |
else: |
os.makedirs(target) |
- linked_names = {}; |
+ linked_names = {}; |
for source in args[1:]: |
# Assume the source directory is named ".../NAME/lib". |
split = source.split(':') |