author | wenzelm |
Tue, 08 Jan 2002 20:52:46 +0100 | |
changeset 12677 | 73c070d5c031 |
parent 10511 | efb3428c9879 |
child 14981 | e73f8140af78 |
permissions | -rwxr-xr-x |
wenzelm@2650 | 1 |
#!/bin/sh |
wenzelm@2650 | 2 |
# |
wenzelm@2650 | 3 |
# $Id$ |
wenzelm@9818 | 4 |
# Author: Markus Wenzel, TU Muenchen |
wenzelm@9818 | 5 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
wenzelm@2650 | 6 |
# |
wenzelm@2650 | 7 |
# configure - adapt Isabelle distribution to system environment |
wenzelm@2650 | 8 |
|
wenzelm@2655 | 9 |
## patch scripts |
wenzelm@2655 | 10 |
|
wenzelm@10511 | 11 |
cd "`dirname "$0"`" |
wenzelm@9915 | 12 |
|
wenzelm@6029 | 13 |
if bash -c : |
wenzelm@2650 | 14 |
then |
wenzelm@10077 | 15 |
bash lib/scripts/patch-scripts.bash |
wenzelm@2650 | 16 |
else |
wenzelm@2650 | 17 |
echo "FATAL ERROR: bash not found!" |
wenzelm@2650 | 18 |
exit 2 |
wenzelm@2650 | 19 |
fi |