From 01d0426553ad3b75f71811773a1e194a32f2f56b Mon Sep 17 00:00:00 2001
From: Andre Anjos <andre.dos.anjos@gmail.com>
Date: Thu, 23 May 2019 12:34:49 +0200
Subject: [PATCH] [scripts/ci] Remove useless echo() calls for docs/ci builds
---
bob/devtools/scripts/ci.py | 5 -----
1 file changed, 5 deletions(-)
diff --git a/bob/devtools/scripts/ci.py b/bob/devtools/scripts/ci.py
index da1ab3b9..a316eaac 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)
--
GitLab