From c9409e7744fbdbb8d8f0a7a04214b680a0360c89 Mon Sep 17 00:00:00 2001
From: Giuseppe Lettieri <g.lettieri@iet.unipi.it>
Date: Fri, 23 Nov 2012 13:58:53 +0100
Subject: [PATCH] set SHELL=/bin/bash, the only shell we have tested

---
 planetlab/exp-tool/Makefile | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/planetlab/exp-tool/Makefile b/planetlab/exp-tool/Makefile
index 32263d4d0..2ec1bc183 100644
--- a/planetlab/exp-tool/Makefile
+++ b/planetlab/exp-tool/Makefile
@@ -3,6 +3,9 @@
 # HOST_<id> and IP_<id> for all nodes involved, as well as 
 # LINKS as a list of <node_id>-<node_id> elements
 
+# should work with any shell, but we have only tested bash
+SHELL=/bin/bash
+
 # run make CONF=anotherconfig.mk if you need several configs
 
 CONF ?= conf.mk
-- 
2.43.0