From eb9a9bf23ddc7260be7f9443bed336d9e2324b7f Mon Sep 17 00:00:00 2001
From: Norman Feske <norman.feske@genode-labs.com>
Date: Sun, 3 Nov 2019 11:51:44 +0100
Subject: [PATCH] bash.run: support using pipes

---
 repos/ports/run/bash.run | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/repos/ports/run/bash.run b/repos/ports/run/bash.run
index f88a61a99e..0e3f37f260 100644
--- a/repos/ports/run/bash.run
+++ b/repos/ports/run/bash.run
@@ -10,6 +10,7 @@ import_from_depot [depot_user]/src/[base_src] \
                   [depot_user]/src/bash \
                   [depot_user]/src/coreutils \
                   [depot_user]/src/vfs \
+                  [depot_user]/src/vfs_pipe \
                   [depot_user]/src/fs_rom
 
 # write default vimrc file
@@ -83,6 +84,7 @@ install_config {
 				<dir name="tmp"> <ram/> </dir>
 				<dir name="dev">
 					<zero/> <null/> <terminal/>
+					<dir name="pipe"> <pipe/> </dir>
 					<inline name="rtc">2018-01-01 00:01</inline>
 				</dir>
 			</vfs>
@@ -105,9 +107,9 @@ install_config {
 
 	<start name="/bin/bash" caps="1000">
 		<resource name="RAM" quantum="30M" />
-		<config>
+		<config ld_verbose="yes">
 			<libc stdin="/dev/terminal" stdout="/dev/terminal"
-			      stderr="/dev/terminal" rtc="/dev/rtc"/>
+			      stderr="/dev/terminal" rtc="/dev/rtc" pipe="/dev/pipe"/>
 			<vfs> <fs/> </vfs>
 			<arg value="bash"/>
 			<env key="TERM" value="screen"/>