diff --git a/workspace_tools/synch.py b/workspace_tools/synch.py index a49f738041..03cfb6776b 100644 --- a/workspace_tools/synch.py +++ b/workspace_tools/synch.py @@ -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