From 054b8de67b758c603d38066535e4535f81cfd8b8 Mon Sep 17 00:00:00 2001 From: Martin Stein Date: Fri, 10 Nov 2017 16:31:21 +0100 Subject: [PATCH] tool/run/grub2: user-friendly missing message Ref #2526 --- tool/run/grub2.inc | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/tool/run/grub2.inc b/tool/run/grub2.inc index 7ab7889be0..787bf2a530 100644 --- a/tool/run/grub2.inc +++ b/tool/run/grub2.inc @@ -7,11 +7,14 @@ proc get_grub2_dir { } { if {![file exists $grub2_path]} { puts "" - puts "GRUB2 binaries are missing." - puts "You can download the GRUB2 binaries by invoking:" - puts "\ttool/ports/prepare_port grub2" + puts "Port not prepared or outdated:" + puts " grub2" + puts "" + puts "You can prepare respectively update it as follows:" + puts " [genode_dir]/tool/ports/prepare_port grub2" puts "" exit 1 } + return $grub2_path }