From 505ff0bb11da526be58bbdd2094212482e1113fb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Josef=20S=C3=B6ntgen?= <josef.soentgen@genode-labs.com>
Date: Wed, 11 Apr 2018 14:28:28 +0200
Subject: [PATCH] ping: exit run script on not supported platforms

Fixes #2756.
---
 repos/os/run/ping.run            | 2 +-
 repos/os/run/ping_nic_router.run | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/repos/os/run/ping.run b/repos/os/run/ping.run
index bd20208a06..bac1017a77 100644
--- a/repos/os/run/ping.run
+++ b/repos/os/run/ping.run
@@ -4,7 +4,7 @@
 
 if {![have_include power_on/qemu]} {
 	puts "Run script is only supported on Qemu"
-	return 0
+	exit 0
 }
 
 set build_components {
diff --git a/repos/os/run/ping_nic_router.run b/repos/os/run/ping_nic_router.run
index 32c57f6e1a..f933e36faf 100644
--- a/repos/os/run/ping_nic_router.run
+++ b/repos/os/run/ping_nic_router.run
@@ -4,7 +4,7 @@
 
 if {![have_include power_on/qemu]} {
 	puts "Run script is only supported on Qemu"
-	return 0
+	exit 0
 }
 
 set build_components {