| author | berghofe | 
| Tue, 16 Oct 2001 19:54:53 +0200 | |
| changeset 11812 | 8d191eaf7fc4 | 
| 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  |