| author | wenzelm | 
| Thu, 28 Sep 2000 19:07:09 +0200 | |
| changeset 10111 | 78a0397eaec1 | 
| parent 10077 | 0261aede52ca | 
| child 10511 | efb3428c9879 | 
| 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$ | 
| 9818 | 4 | # Author: Markus Wenzel, TU Muenchen | 
| 5 | # License: GPL (GNU GENERAL PUBLIC LICENSE) | |
| 2650 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 6 | # | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 7 | # configure - adapt Isabelle distribution to system environment | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 8 | |
| 2655 | 9 | ## patch scripts | 
| 10 | ||
| 10077 | 11 | cd `dirname "$0"` | 
| 9915 | 12 | |
| 6029 | 13 | if bash -c : | 
| 2650 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 14 | then | 
| 10077 | 15 | bash lib/scripts/patch-scripts.bash | 
| 2650 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 16 | else | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 17 | echo "FATAL ERROR: bash not found!" | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 18 | exit 2 | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 19 | fi |