diff --git a/bob/devtools/scripts/ci.py b/bob/devtools/scripts/ci.py index da1ab3b9e1d9f3dc975beaea49f9ad9bd88d43ec..a316eaac28f66ab6ed084eb4aad4b71add531a9a 100644 --- a/bob/devtools/scripts/ci.py +++ b/bob/devtools/scripts/ci.py @@ -672,11 +672,6 @@ def docs(ctx, requirement, dry_run): for n, (package, branch) in enumerate(packages): - echo_normal('\n' + (80*'=')) - echo_normal('Getting %s@%s (%d/%d)' % (package, branch, n+1, - len(packages))) - echo_normal((80*'=') + '\n') - group, name = package.split('/', 1) clone_to = os.path.join(doc_path, group, name)