| author | paulson | 
| Wed, 21 Jul 1999 15:23:18 +0200 | |
| changeset 7058 | 8dfea70eb6b7 | 
| parent 6029 | 30c957a74803 | 
| child 9818 | 71de955e8fc9 | 
| 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  | 
||
| 6029 | 9  | 
if bash -c :  | 
| 
2650
 
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  |