author | paulson |
Thu, 05 Sep 2002 14:03:03 +0200 | |
changeset 13559 | 51c3ac47d127 |
parent 10511 | efb3428c9879 |
child 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 |
5 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
2650
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
6 |
# |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
7 |
# configure - adapt Isabelle distribution to system environment |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
8 |
|
2655 | 9 |
## patch scripts |
10 |
||
10511 | 11 |
cd "`dirname "$0"`" |
9915 | 12 |
|
6029 | 13 |
if bash -c : |
2650
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
14 |
then |
10077 | 15 |
bash lib/scripts/patch-scripts.bash |
2650
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
16 |
else |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
17 |
echo "FATAL ERROR: bash not found!" |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
18 |
exit 2 |
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
19 |
fi |