From 4af7b1c9a94d26a95bb4c373b8ce1a6f300454f1 Mon Sep 17 00:00:00 2001
From: Jose Luis Contreras <joseluis.contreras.santos@gmail.com>
Date: Thu, 6 Dec 2018 14:19:28 +0100
Subject: [PATCH] Update dev_menu.py

Co-Authored-By: larroy <pedro.larroy.lists@gmail.com>
---
 dev_menu.py | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/dev_menu.py b/dev_menu.py
index 0a1c7a7e2246..4b6de4cb42cf 100755
--- a/dev_menu.py
+++ b/dev_menu.py
@@ -151,9 +151,7 @@ def clip(x, mini, maxi):
 
 @retry((ValueError, RuntimeError), 3, delay_s = 0)
 def show_menu(items: List[str], header=None) -> int:
-    print()
-    print('-- MXNet dev menu --')
-    print()
+    print('\n-- MXNet dev menu --\n')
     def hr():
         print(''.join(['-']*30))
     if header: