From fa3cca3fb0ab957604a29feda734f5bc7db7afdc Mon Sep 17 00:00:00 2001 From: Karolin Seeger Date: Wed, 29 May 2013 10:23:49 +0200 Subject: [PATCH] build-htmlman-git: Run build-htmlman-git with bash. On debian/ubuntu, the "dash" which is sh, does not provide pushd/popd... Signed-off-by: Karolin Seeger Reviewed-by: Andrew Bartlett --- release-scripts/build-htmlman-git | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/release-scripts/build-htmlman-git b/release-scripts/build-htmlman-git index 50707a4f17e..d85c703f4e1 100755 --- a/release-scripts/build-htmlman-git +++ b/release-scripts/build-htmlman-git @@ -1,4 +1,4 @@ -#!/bin/sh +#!/bin/bash # # Copyright (C) Michael Adam 2011 #