| author | wenzelm | 
| Mon, 17 Apr 2000 14:07:00 +0200 | |
| changeset 8724 | ef7efded8fdc | 
| 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 |