blob: 4ece1175bd5481c7f1ff2f14b55dc7cd2a831057 (
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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
--- lib/scripts/run-polyml-5.0.orig Sun Oct 21 04:32:23 2007
+++ lib/scripts/run-polyml-5.0 Sat Jan 12 18:01:28 2008
@@ -1,22 +1,20 @@
-#!/usr/bin/env bash
+#!/bin/sh
#
# $Id: run-polyml-5.0,v 1.9 2007/10/20 18:32:23 wenzelm Exp $
# Author: Makarius
#
# Poly/ML startup script (for 5.0)
-export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
-
## diagnostics
-function fail_out()
+fail_out()
{
echo "Unable to create output heap file: \"$OUTFILE\"" >&2
exit 2
}
-function check_file()
+check_file()
{
if [ ! -f "$1" ]; then
echo "Unable to locate $1" >&2
@@ -25,6 +23,21 @@
fi
}
+SAVE_INFILE="$INFILE"
+SAVE_OUTFILE="$OUTFILE"
+SAVE_COPYDB="$COPYDB"
+SAVE_COMPRESS="$COMPRESS"
+SAVE_MLTEXT="$MLTEXT"
+SAVE_TERMINATE="$TERMINATE"
+SAVE_NOWRITE="$NOWRITE"
+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
+INFILE="$SAVE_INFILE"
+OUTFILE="$SAVE_OUTFILE"
+COPYDB="$SAVE_COPYDB"
+COMPRESS="$SAVE_COMPRESS"
+MLTEXT="$SAVE_MLTEXT"
+TERMINATE="$SAVE_TERMINATE"
+NOWRITE="$SAVE_NOWRITE"
## compiler executables and libraries
|
