| author | huffman |
| Wed, 02 Mar 2005 00:56:41 +0100 | |
| changeset 15557 | 2901b1f6ba64 |
| parent 14981 | e73f8140af78 |
| 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$ |
| 9818 | 4 |
# Author: Markus Wenzel, TU Muenchen |
|
2650
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
5 |
# |
|
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
6 |
# configure - adapt Isabelle distribution to system environment |
|
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
7 |
|
| 2655 | 8 |
## patch scripts |
9 |
||
| 10511 | 10 |
cd "`dirname "$0"`" |
| 9915 | 11 |
|
| 6029 | 12 |
if bash -c : |
|
2650
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
13 |
then |
| 10077 | 14 |
bash lib/scripts/patch-scripts.bash |
|
2650
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
15 |
else |
|
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
16 |
echo "FATAL ERROR: bash not found!" |
|
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
17 |
exit 2 |
|
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
18 |
fi |