--- ./lib/Tools/browser.orig Sun Sep 2 15:11:55 2007 +++ ./lib/Tools/browser Sun Sep 2 15:47:49 2007 @@ -1,4 +1,4 @@ -#!/usr/bin/env bash +#!/bin/sh # # $Id: browser,v 1.16 2004/06/21 08:25:57 kleing Exp $ # Author: Markus Wenzel, TU Muenchen @@ -8,7 +8,7 @@ PRG="$(basename "$0")" -function usage() +usage() { echo echo "Usage: $PRG [OPTIONS] [GRAPHFILE]" @@ -20,7 +20,7 @@ exit 1 } -function fail() +fail() { echo "$1" >&2 exit 2