summaryrefslogtreecommitdiff
path: root/math/isabelle/files/patch-lib-Tools-makeall
blob: 01a5e28d69ebe7b63839dc68a269b21946c51a4d (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/makeall.orig	Sat Jan 12 16:57:16 2008
+++ lib/Tools/makeall	Sat Jan 12 17:01:23 2008
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/sh
 #
 # $Id: makeall,v 1.20 2005/12/01 17:41:46 wenzelm Exp $
 # Author: Markus Wenzel, TU Muenchen
@@ -14,7 +14,7 @@
 
 PRG="$(basename "$0")"
 
-function usage()
+usage()
 {
   echo
   echo "Usage: $PRG [ARGS ...]"
@@ -24,7 +24,7 @@
   exit 1
 }
 
-function fail()
+fail()
 {
   echo "$1" >&2
   exit 2