author | nipkow |
Thu, 27 Mar 1997 17:46:24 +0100 | |
changeset 2846 | 53c76f9d95fd |
parent 2754 | 59bd96046ad6 |
child 3007 | e5efa177ee0c |
permissions | -rwxr-xr-x |
2650
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
1 |
#!/bin/sh |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
2 |
# |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
3 |
# $Id$ |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
4 |
# |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
5 |
# configure - adapt Isabelle distribution to system environment |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
6 |
|
2655 | 7 |
## patch scripts |
8 |
||
2650
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
9 |
if bash -norc -c "" |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
10 |
then |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
11 |
bash lib/scripts/patch-scripts.bash |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
12 |
else |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
13 |
echo "FATAL ERROR: bash not found!" |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
14 |
exit 2 |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
15 |
fi |