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

Fix synchronization script

pull/258/head mbed_lib_rev82
Bogdan Marinescu 2014-04-07 17:35:18 +01:00
parent 0a55118494
commit b7ce2ee5bf
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

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