blob: beebd48dc0f786fb9beced9795a85c6d1341584a (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
--- lib/Tools/display.orig Sat Jan 12 16:57:02 2008
+++ lib/Tools/display Sat Jan 12 17:00:11 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: display,v 1.10 2006/11/13 17:19:24 wenzelm Exp $
# Author: Markus Wenzel, TU Muenchen
@@ -8,7 +8,7 @@
PRG="$(basename "$0")"
-function usage()
+usage()
{
echo
echo "Usage: $PRG [OPTIONS] FILE"
@@ -21,7 +21,7 @@
exit 1
}
-function fail()
+fail()
{
echo "$1" >&2
exit 2
|
