ARMmbed
/
mbed-os
mirror of https://github.com/ARMmbed/mbed-os.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Fix error in 'update_repo' call

pull/92/head^2
Bogdan Marinescu 2013-10-23 17:27:36 +03:00
parent 2404dc0092
commit 6af18d0946
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
workspace_tools/synch.py
View File

@ -296,7 +296,7 @@ def update_dependencies(repositories):
def update_mbed(): def update_mbed():
update_repo("mbed", join(BUILD_DIR, "mbed")) update_repo("mbed", [join(BUILD_DIR, "mbed")])
def do_sync(options): def do_sync(options):
global push_remote, quiet, commit_msg, changed global push_remote, quiet, commit_msg, changed