From 2bd728e45eacceca88762a879d72b570dd1a9536 Mon Sep 17 00:00:00 2001
From: Jean-Paul Chaput <Jean-Paul.Chaput@lip6.fr>
Date: Mon, 7 May 2012 14:43:35 +0000
Subject: [PATCH] Under Ubuntu, push/popd are present only if we invoke bash,
 not sh.

---
 alliance/src/documentation/regression.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/alliance/src/documentation/regression.sh b/alliance/src/documentation/regression.sh
index 206500f6..3f78a7f1 100755
--- a/alliance/src/documentation/regression.sh
+++ b/alliance/src/documentation/regression.sh
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 
  if [ -z "$ALLIANCE_TOP" ]; then
    alcEnv="/etc/profile.d/alc_env.sh"