| author | nipkow | 
| Thu, 01 Oct 1998 18:30:44 +0200 | |
| changeset 5602 | 5293b6f5c66c | 
| 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 |