| author | paulson | 
| Mon, 01 Dec 1997 12:52:18 +0100 | |
| changeset 4331 | 34bb65b037dd | 
| parent 3007 | e5efa177ee0c | 
| child 6029 | 30c957a74803 | 
| 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  | 
||
| 3007 | 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  |