| author | wenzelm | 
| Mon, 18 Jan 1999 21:12:42 +0100 | |
| changeset 6136 | 166b3353aad5 | 
| 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 |